たいぷしのにむで部分適用したい

けど出来ないので次のようになってしまう・・・。

{-# LANGUAGE KindSignatures,
  TypeFamilies,
  EmptyDataDecls,
  MultiParamTypeClasses,
  FunctionalDependencies,
  UndecidableInstances,
  TypeOperators,
  FlexibleInstances
  #-}

data Nil
data Cons a b
type a :<: b = Cons a b
infixr 7 :<:

type family Map (f :: * -> *) l
type instance Map f Nil = Nil
type instance Map f (Cons a b) = Cons (f a) (Map f b)

data Zero
data Succ a
data Add a b

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three

class Force a b | a -> b where
    getType :: a -> b
instance Force Zero Zero
instance (Force a b) => Force (Succ a) (Succ b)
instance (Force a b) => Force (Add Zero a) b
instance (Force a c,Force b d,Force (Add c d) e) => Force (Add (Succ a) b) (Succ e)
instance Force Nil Nil
instance (Force a c,Force b d) => Force (Cons a b) (Cons c d)

type Ty1 = Add Four Three
type Ty2 = Map (Add One) (One :<: Two :<: Nil)
{-

:t getType (undefined :: Ty1) -- これで型が見える
:t getType (undefined :: Ty2) -- これで型が見える

-}

悲しい・・・。

本当はどうしたいかというと

type family Add a b :: *
type instance Add Zero b = b
type instance Add (Succ a) b = Succ (Add a b)

type Ty2 = Map (Add One) (One :<: Two :<: Nil)

これだとAddに2つ引数をその場で渡してあげないといけないにもかかわらず、Oneしか出ていない為に、エラー。ので自然に解決したいとすると、気持ちとしてはType Synonymで部分適用出来て欲しいよなーという事なんですけれども・・・。

もしかしてこうしたら良いんじゃね??

{-# LANGUAGE KindSignatures,
  TypeFamilies,
  EmptyDataDecls,
  MultiParamTypeClasses,
  FunctionalDependencies,
  UndecidableInstances,
  TypeOperators,
  FlexibleInstances,
  TypeSynonymInstances
  #-}

data Nil
data Cons a b
type a :<: b = Cons a b
infixr 7 :<:

type family Map (f :: * -> *) l
type instance Map f Nil = Nil
type instance Map f (Cons a b) = Cons (f a) (Map f b)

data Zero
data Succ a
data Add a b

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three

type family TAdd a b :: *
type instance TAdd Zero b = b
type instance TAdd (Succ a) b = Succ (TAdd a b)

class Force a b | a -> b where
    getType :: a -> b
instance Force Zero Zero
instance (Force a b) => Force (Succ a) (Succ b)
-- instance (Force a b) => Force (Add Zero a) b
-- instance (Force a c,Force b d,Force (Add c d) e) => Force (Add (Succ a) b) (Succ e)
instance (Force a c,Force b d,Force (TAdd c d) e) => Force (Add a b) e
instance Force Nil Nil
instance (Force a c,Force b d) => Force (Cons a b) (Cons c d)

type Ty1 = Add Four Three
type Ty2 = Map (Add One) (One :<: Two :<: Nil)

これだと実装をType Familyで行えて、Addを被せるだけみたいな！！

うーんこれだなぁ。
後は型クラスForceをもうちょっとうまく・・・なんか・・・。

参考

http://twitter.com/shelarcy/status/6174257809
http://twitter.com/shelarcy/status/6171119681
http://hpaste.org/fastcgi/hpaste.fcgi/view?id=13349