swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
Tip revision: b6407e0f026cf5491ca5ed0a35ea5cf316ebe8ca authored by Anish Tondwalkar on 21 May 2021, 03:15:25 UTC
formatted for submission
formatted for submission
Tip revision: b6407e0
linearTypes.hs
undefined as rforall a. a
undefined = 0
var as x:Int -> (Lin >{v:Set >Int | v = setPlus emptySet x})
var = undefined
fun as env:(Set >Int) ~> n:{v:Int | (v ∈ env) ≠ True} -> (Lin >{v:Set >Int | v = setPlus env n}) -> (Lin >{v:Set >Int | v = env})
fun = undefined
app as env1:(Set >Int) ~> env2:{v:Set >Int | env1 ∩ v = emptySet} ~> (Lin >{v:Set >Int | v = env1}) -> (Lin >{v:Set >Int | v = env2}) -> (Lin >{v:Set >Int | v = env1 ∪ env2})
app = undefined
typecheck as (Lin >{v:Set >Int | v = emptySet}) -> (Lin >(Set >Int))
typecheck = undefined
program1 :: Lin >(Set >Int)
program1 = typecheck (fun 1 (app (var 1) (var 1)))
program2 :: Lin >(Set >Int)
program2 = typecheck (fun 1 (fun 2 (fun 3 (app (var 1) (var 2)))))