Last active
February 18, 2019 00:31
-
-
Save dylnb/d3ad4e883f0a8e5f65805959e538e903 to your computer and use it in GitHub Desktop.
testing dependent currying
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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))) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment