我有一个类型级别的数字
data Z deriving Typeable
data S n deriving Typeable
和 n 元函数(来自固定向量包的代码)
-- | 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)
我读了几篇关于类型级别计算的文章,但都是关于类型安全列表串联的。
这在打开/重新包装时需要小心一些Fun
新类型。我还利用了DataKinds
扩大。
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies,
MultiParamTypeClasses, ScopedTypeVariables, FlexibleInstances #-}
{-# OPTIONS -Wall #-}
-- | Type-level naturals.
data Nat = Z | S Nat
-- | Type family for n-ary functions.
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
-- | Addition.
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 wrapper which is used to make 'Fn' injective.
newtype Fun n a b = Fun { unFun :: Fn n a b }
class UncurryN (n :: Nat) (m :: Nat) a b where
uncurryN :: Fun (Add n m) a b -> Fun n a (Fun m a b)
instance UncurryN Z m a b where
uncurryN g = Fun g
instance UncurryN n m a b => UncurryN (S n) m a b where
uncurryN g = Fun (\x -> unFun (uncurryN (Fun (unFun g x)) :: Fun n a (Fun m a b)))
{- An expanded equivalent with more signatures:
instance UncurryN n m a b => UncurryN (S n) m a b where
uncurryN g = let f :: a -> Fn n a (Fun m a b)
f x = let h :: Fun (Add n m) a b
h = Fun ((unFun g :: Fn (Add (S n) m) a b) x)
in unFun (uncurryN h :: Fun n a (Fun m a b))
in Fun f
-}
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)