Uncurry per funzioni n-ario

Question

Ho un numero di livello a

data Z deriving Typeable 
data S n deriving Typeable 

e n-ario funzioni (codice dal pacchetto-vector fissa)

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

ho bisogno funzione come

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

Ho letto diversi articoli sui calcoli a livello di caratteri, ma tutto sulla concatenazione di tipo lista sicura.

Answer 1

È possibile farlo senza alcun tipo classi con la costruzione di un tipo di dati che può rappresentare il tipo Nat a livello di dati:

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

Se non ti piace menzionare in modo esplicito il parametro n, questo è ok dato che puoi sempre andare avanti e indietro tra una funzione che accetta un parametro come una classe di tipo e che prende un parametro come dati:

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 

Answer 2

Ciò ha richiesto un po 'di attenzione nello scartare/riavvolgere il nuovo tipo Fun. Ho anche sfruttato l'estensione 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 
-}