Uncurry для n-арных функций

У меня есть номер уровня типа

data Z   deriving Typeable
data S n deriving Typeable

и n-арные функции (код из пакета fixed-vector)

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

Я прочитал несколько статей о вычислениях на уровне типов, но все о конкатенации безопасных списков типов.


person user3856365    schedule 19.07.2014    source источник
comment
Введите конкатенацию безопасных списков? С каких это пор стандартный небезопасен?   -  person Piotr Miś    schedule 19.07.2014
comment
@uraf Возможно, это из-за разнородных списков.   -  person AndrewC    schedule 20.07.2014


Ответы (2)


Вы можете сделать это без каких-либо классов типов, создав тип данных, который может представлять тип 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
person user2407038    schedule 19.07.2014

Это потребовало некоторой осторожности при развертывании/перепаковывании нового типа 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
-}
person chi    schedule 19.07.2014
comment
Обратите внимание, что вы повторяете только параметры n, и в каждом случае a, b, m совершенно бесплатны. Это показатель того, что они не должны быть параметрами класса UncurryN, они должны быть свободными переменными. Это улучшит вывод типов при использовании uncurryN : если все они являются параметрами, компилятор будет думать, что они имеют значение для выбранного класса, и потребует, чтобы они были мономорфными или упоминались явно. - person user2407038; 20.07.2014