如何使用 withKnownNat 将值提升到类型中

Question

我在

withKnownNat

中找到了函数

withSomeSNat

和

GHC.TypeNats

。根据它们的签名，可以将函数应用于动态类型参数。如果不可能那么拥有这些功能的目的是什么？实际例子不多

withSomeSNat :: Natural -> (forall (n :: Nat). SNat n -> r) -> r 
withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r 

第一次尝试组合这些函数时遇到了类型检查器的抱怨。

 dynat :: [()]
 dynat = withSomeSNat 3 (`withKnownNat` props)

 props :: forall n. KnownNat n => [()]
 props = []

无法推断出因使用“props”而产生的“KnownNat n0” 上下文：KnownNat n 由上下文期望的类型绑定： KnownNat n => [()]

Answer 1

props

的类型签名使得类型变量

n

不明确。 一种解决方案是编写如下内容：

dynat :: [()]
dynat = withSomeSNat 3 go
  where go :: forall n. SNat n -> [()]
        go s = withKnownNat s $ props @n

props :: forall n. KnownNat n => [()]
props = []

请注意，如果

props

具有明确的类型，那么您原来的方法就可以正常工作：

{-# LANGUAGE DataKinds #-}

module Nats where

import GHC.TypeNats

data Foo n = Foo

dynat :: Foo 3
dynat = withSomeSNat 3 (`withKnownNat` props)

props :: forall n. KnownNat n => Foo n
props = Foo