放弃n元功能 [英] Uncurry for n-ary functions

问题描述

我有一个类型级数字

I have a type level numbers

data Z   deriving Typeable
data S n deriving Typeable

和n元函数（来自固定矢量包的代码）

and n-ary functions (code from fixed-vector package)

-- | 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)

我读过几篇关于类型级计算的文章，但都是关于类型安全列表串联。

I read several articles about type level computations, but all about type safe list concatenation.

推荐答案

您可以通过构建可表示类型的数据类型， Nat 在数据层面上：

You can do this without any type classes by constructing a datatype which can represent the type Nat on the data level:

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 参数，这是可以的，因为你总是可以在一个函数中来回访问函数，该函数将参数作为类型类并将参数作为数据： p>

If you don't like explicitly mentioning the n parameter, thats ok since you can always go back and forth between a function which takes an parameter as a type class and which takes a parameter as data:

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

这篇关于放弃n元功能的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！