型レベルで計算するやつ

a.hs

{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE ExplicitForAll         #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances   #-}

module Main where

import Control.Applicative

-- No argument
data N = N

data S a b c where
  S :: S N N N

data K a b where
  K :: K N N

class Term a where
  term :: a b c
  term = undefined

-- 型を評価
class Eval a b | a -> b where
  eval :: a -> b
  eval = undefined

instance Term (S N)
instance Term K

instance forall a b c. (Term a, Term b) => Eval (S N N N) (a N N -> b N N -> c -> a c (b c N))
instance forall a b. Eval (K N N) (a -> b -> a)
instance forall a b ax ay. (Term a) => Eval (K (a ax ay) N) (b -> a ax ay)
instance forall a b ax ay bx by. (Term a, Term b) => Eval (K (a ax ay) (b bx by)) (a ax ay)

-- 型を値に戻す
class IsRuntime a b | a -> b where
  fromType :: a -> b

instance forall a b c. IsRuntime (S N N N) ((c -> b -> a) -> (c -> b) -> c -> a) where
  fromType _ = (<*>)

instance forall a b. IsRuntime (K N N) (a -> b -> a) where
  fromType _ = const