为什么Haskell不能推断这种类型是正确的？

Question

我有一个简单的Nat定义和由Nat's,Natty索引的类型定义.

data Nat :: * where 
    Zero :: Nat
    Suc  :: Nat -> Nat

data Natty :: Nat -> * where
    Zy :: Natty Zero
    Sy :: Natty n -> Natty (Suc n)

我的目标是创建一个函数,给定由Nat n索引的类型和由Nat m索引的类型,将生成一个由Nat n + m类型索引的类型.

例如,foo(Sy Zy)(Sy $ Sy Zy)= Sy $ Sy $ Sy Zy

Nat添加很简单,定义如下:

nAdd :: Nat -> Nat -> Nat
nAdd x  Zero    = x
nAdd x (Suc y)  = Suc $ nAdd x y

我原以为foo会以下列方式定义:

foo :: Natty n -> Natty m -> Natty (nAdd n m)
foo x  Zy    = x
foo x (Sy y) = Sy $ foo x y 

但这会导致一个有趣的错误:

Could not deduce: n ~ nAdd n 'Zero
from the context: m ~ 'Zero

为什么haskell不能推断出n~nAdd n'Zero？有没有一种简单的方法可以解决这个问题,还是需要采用不同的方法？

谢谢,任何输入将不胜感激.还使用以下扩展名.

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-} 

Answer 1

正如@AlexisKing所指出的nAdd那样,类型签名中的for foo只被视为另一个类型变量(如m或n),而Haskell并没有将它绑定回函数的定义nAdd.

在Haskell中,您不能将术语级函数(如nAdd)应用于类型.相反,您需要使用类型系列.如果将类型级"函数" NAdd定义为类型族:

type family NAdd (a :: Nat) (b :: Nat) :: Nat
type instance NAdd n Zero = n
type instance NAdd n (Suc m) = Suc (NAdd n m)

然后你可以在你的foo签名中使用这个功能:

foo :: Natty n -> Natty m -> Natty (NAdd n m)
foo x  Zy    = x
foo x (Sy y) = Sy $ foo x y 

这需要许多额外的扩展才能工作,完整的工作示例(在GHC 8.2.2下运行)如下所示:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind

data Nat :: * where 
    Zero :: Nat
    Suc  :: Nat -> Nat

data Natty :: Nat -> * where
    Zy :: Natty Zero
    Sy :: Natty n -> Natty (Suc n)

type family NAdd (a :: Nat) (b :: Nat) :: Nat
type instance NAdd n Zero = n
type instance NAdd n (Suc m) = Suc (NAdd n m)

nAdd :: Nat -> Nat -> Nat
nAdd x  Zero    = x
nAdd x (Suc y)  = Suc $ nAdd x y

foo :: Natty n -> Natty m -> Natty (NAdd n m)
foo x  Zy    = x
foo x (Sy y) = Sy $ foo x y 

test1 = foo (Sy Zy) (Sy $ Sy Zy)
test2 = Sy $ Sy $ Sy Zy