是否有可能写一个函数Int - > NatSing n,其中NatSing是单个类型的peano数？

Question

对于模糊标题的道歉,这里有一些背景:http://themonadreader.files.wordpress.com/2013/08/issue221.pdf

上述问题中的GADT文章介绍了Nat类型和用于各种类型级列表函数的natSing类型(concat,!!,head,repeat等).对于其中的几个函数,有必要创建类型族来定义Nat类型的+和<.

data Nat = Zero | Succ Nat

data NatSing (n :: Nat) where
    ZeroSing :: NatSing Zero
    SuccSing :: NatSing n -> NatSing (Succ n)

data List (n :: Nat) a where
    Nil  :: List n a
    Cons :: a -> List n a -> List (Succ n) a

无论如何,我已经编写了一个函数"list",它将普通[a]转换为a List n a,以方便调用者.这需要列表的长度作为输入,就像repeat(来自链接文章):

list :: [a] -> NatSing n -> List n a
list []      ZeroSing    = Nil
list (x:xs) (SuccSing n) = Cons x (list xs n)
list _       _           = error "length mismatch"

使用辅助函数会很好toNatSing :: Int -> NatSing n,所以上面的内容可以写成

list :: [a] -> List n a
list xs = list' xs (toNatSing $ length xs)
  where
    list' :: [a] -> NatSing n -> List n a
    list' = ... -- same as before, but this time I simply "know" the function is no longer partial

是否可以编写这样的功能toNatSing？我一直在与类型摔跤,还没有想出任何东西.

非常感谢!

Answer 1

不,你不能写这样的功能.

类型的功能

Int -> NatSing n

说它可以将任何整数转换为多态 NatSing.但是没有多态性NatSing.

你在这里想要的是n由传入决定的Int.这是一个依赖类型:

(n :: Int) -> NatSing n

在Haskell中这样的事情是不可能的.您必须使用Agda或Idris或其他依赖类型的语言.对单身人士的黑客攻击正是哈斯克尔解决这个问题的方法.如果要根据值进行区分,则必须将值提升到类型级别,即此类型NatSing.

您可以通过将其包装为存在类型来编写一个NatSing为某些 函数返回的函数:nn

data ExNatSing where
  ExNatSing :: NatSing n -> ExNatSing

但这在实践中不会给你带来太多好处.通过打包n,您将丢失有关它的所有信息,并且以后无法根据它做出决定.

通过完全相同的参数,您也可以不希望定义一个函数

list :: [a] -> List n a

您可以用来保存自己的一些打字工作的唯一方法是定义一个NatSing自动构造值的类型类:

class CNatSing (n :: Nat) where
  natSing :: NatSing n

instance CNatSing Zero where
  natSing = ZeroSing

instance CNatSing n => CNatSing (Succ n) where
  natSing = SuccSing natSing

然后,你可以说:

list :: CNatSing n => [a] -> List n a
list xs = list' xs natSing
  where
    list' :: [a] -> NatSing n -> List n a
    list' = ... -- same as before, but still partial

在这里,您使用它的类型上下文使GHC填充在右侧NatSing.但是,这个功能仍然是局部的,因为函数的调用者仍然可以选择n使用它.如果我想使用一个[Int]长度3,List (Succ Zero) Int它会崩溃.

再一次,你可以把它包装在一个存在主义中:

data SomeList a where
  SomeList :: NatSing n -> List n a -> SomeList a

然后你可以写

list :: [a] -> SomeList a
list []       = SomeList ZeroSing Nil
list (x : xs) = case list xs of
                  SomeList n xs -> SomeList (SuccSing n) (x : xs')

同样,好处很小,但相比之下ExNatSing,至少有一个:您现在可以暂时解包SomeList并将其传递给在a上运行的函数List n a,获取类型系统保证如何通过这些转换列表的长度功能.