cps.hs
bind as rforall a, b, p, q, r.
M <p >q >a ->
(underscore:a -> M <q >r >b) ->
M <p >r >b
bind = 0
magic as rforall a. a
magic = 0
foo as x:Int ~> underscore:Int -> M <Int >{v:Int | v = x} >{v:Int | v = x}
foo = \underscore -> magic
bar as x:Int -> M <{v:Int | v = x} >{v: Int | v = x} >Int
bar = 0
main :: M <Int >Int >Int
main =
bind (foo 0) (\x -> bar x)
foo2 :: rforall a.
underscore:Int ->
(x:Int ~> (M <Int >{v:Int | v = x} >{v:Int | v = x}) -> a) ->
a
foo2 = \underscore -> (\k -> let thinged = magic in k thinged)
main2 :: M <Int >Int >Int
main2 =
foo2 0 (\mx ->
bind mx (\x -> bar x))
-- incr :: n:Int ~> (Int -> { v : Int | v == n }) -> { v : Int | v == n + 1 }
-- incr = \ f -> (f 0) + 1
-- test1 :: { v : Int | v == 11 }
-- test1 = incr (\x -> 10)