不具备n-ary功能

Question

我有一个类型级别的数字

data Z   deriving Typeable
data S n deriving Typeable

和n-ary函数(来自固定向量包的代码)

-- | Type family for n-ary functions.
type family   Fn n a b
type instance Fn Z     a b = b
type instance Fn (S n) a b = a -> Fn n a b

-- | Newtype wrapper which is used to make 'Fn' injective. It's also a
--   reader monad.
newtype Fun n a b = Fun { unFun :: Fn n a b }

我需要像这样的功能

uncurryN :: Fun (n + k) a b -> Fun n a (Fun k a b)

我读了几篇关于类型级计算的文章,但都是关于类型安全列表连接的.

Answer 1

Nat您可以通过构造可以在数据级别表示类型的数据类型来在没有任何类型类的情况下完成此操作：

data Nat = Z | S Nat

type family   Fn (n :: Nat) a b
type instance Fn Z     a b = b
type instance Fn (S n) a b = a -> Fn n a b

type family   Add (n :: Nat) (m :: Nat) :: Nat
type instance Add Z          m = m
type instance Add (S n)      m = S (Add n m)

newtype Fun n a b = Fun { unFun :: Fn n a b }

data SNat (n :: Nat) where 
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

uncurryN :: forall n m a b . SNat n -> Fun (Add n m) a b -> Fun n a (Fun m a b) 
uncurryN SZ f = Fun f
uncurryN (SS (n :: SNat n')) g = Fun (\x -> unFun (uncurryN n (Fun (unFun g x)) :: Fun n' a (Fun m a b)))

如果您不喜欢明确提及n参数，那也没关系，因为您始终可以在将参数作为类型类的函数和将参数作为数据的函数之间来回切换：

class SingI (a :: k) where
  type Sing :: k -> * 
  sing :: Sing a

instance SingI Z where 
  type Sing = SNat
  sing = SZ

instance SingI n => SingI (S n) where
  type Sing = SNat
  sing = SS sing 

toNatSing :: (SNat n -> t) -> (SingI n => t)
toNatSing f = f sing 

fromNatSing :: (SingI n => t) -> (SNat n -> t)
fromNatSing f SZ = f 
fromNatSing f (SS n) = fromNatSing f n 

uncurryN' :: SingI n => Fun (Add n m) a b -> Fun n a (Fun m a b) 
uncurryN' = toNatSing uncurryN