testing dependent currying

Paychecks.hs

{-# LANGUAGE GADTs, FlexibleInstances #-}

module Paychecks where

type E = String

data Z
data S n

data Arity k where
  Ret :: E -> Arity Z
  App :: (E -> Arity n) -> Arity (S n)

instance Show (Arity Z) where
  show (Ret x) = x

type Pro k = Arity k -> Arity k

him0 :: Pro Z
him0 = id

him1 :: Pro (S Z)
him1 = id

him2 :: Pro (S (S Z))
him2 = id

f :: Arity (S (S Z))
f = App (\x -> App (\y -> Ret $ y ++ x))

app :: Arity (S n) -> E -> Arity n
app (App h) = h

test = app (app f "x") "y"

-- > :t test
-- test :: Arity Z
-- > test
-- yx

him :: Pro k
him = id

-- > :t him
-- him :: Pro a
-- > :t him f
-- him f :: Arity (S (S Z))

hm = him (App (\x -> App (\y -> App (\z -> Ret $ z ++ y ++ x))))
-- > :t hm
-- hm :: Arity (S (S (S Z)))