An implementation of System F, System Fsub (F_{<:}) and Finter (F_∧)
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
src
test
.gitignore
LICENSE
LambdaQuest.cabal
README.md
Setup.hs
stack.yaml

README.md

LambdaQuest

This is an implementation of System F, System F<: (Fsub) and F (Finter), with

  • primitive types: Int, Real, Bool, Unit
  • primivite values: integer literals, floating point literals, True, False, unit
  • built-in functions:
negateInt : Int -> Int
negateReal : Real -> Real
intToReal : Int -> Real
addInt, subInt, mulInt : Int -> Int -> Int
ltInt, leInt, equalInt : Int -> Int -> Bool
addReal, subReal, mulReal, divReal : Real -> Real -> Real
ltReal, leReal, equalReal : Real -> Real -> Bool
negate : Int -> Int & Real -> Real                         [Finter only]
add, sub, mul: Int -> Int -> Int & Real -> Real -> Real    [Finter only]
  • non-trivial subtyping relation of primitives: Int <: Real [Fsub and Finter only]

Example

  • readline is required to build REPL program.

Play with System F:

$ stack build
$ stack exec SystemF-repl
This is System F REPL.
Press Ctrl-D to exit.
> \x: Int. x
Type is Int -> Int.
Evaluation:
\x:Int. x
--> \x:Int. x.
> (\x: Int. x) 123
Type is Int.
Evaluation:
(\x: Int. x) 123
--> 123.
> (?a. (\x: a. x)) [Int] 123
Type is Int.
Evaluation:
(?a. \x:a. x) [Int] 123
--> (\x:Int. x) 123
--> 123.
> let id = ?a. \x:a. x in id [Int -> Int] (id [Int])
Type is Int -> Int.
Evaluation:
let id = ?a. \x:a. x in id [Int -> Int] (id [Int])
--> (?a. \x:a. x) [Int -> Int] ((?a. \x:a. x) [Int])
--> (\x:Int -> Int. x) ((?a. \x:a. x) [Int])
--> (\x:Int -> Int. x) (\x:Int. x)
--> \x:Int. x.
> ^D
Bye!

Play with System Fsub:

$ stack exec SystemFsub-repl
This is System Fsub REPL.
Press Ctrl-D to exit.
> (\x: Int. addReal x 1.0) 3
Type is Real.
Evaluation:
(\x:Int. addReal x 1.0) 3
--> addReal 3 1.0
--> 4.0.
> (?a<:Real. \x:a. addReal x x) [Int] 5
Type is Real.
Evaluation:
(?a<:Real. \x:a. addReal x x) [Int] 5
--> (\x:Int. addReal x x) 5
--> addReal 5 5
--> 10.0.
> (\f:Int -> Real. f 4) negateInt
Type is Real.
Evaluation:
(\f:Int -> Real. f 4) negateInt
--> negateInt 4
--> -4.
> ^D
Bye!

Play with Finter:

$ stack exec Finter-repl
> let double = for a in Int, Real. \x:a. add x x
double : Int -> Int & Real -> Real.
Evaluation:
for a in Int, Real. \x:a. add x x
--> \x:Top. add x x.
> double 1
Type is Int.
Evaluation:
double 1
--> (\x:Top. add x x) 1
--> add 1 1
--> 2.
> double 2.0
Type is Real.
Evaluation:
double 2.0
--> (\x:Top. add x x) 2.0
--> add 2.0 2.0
--> 4.0.
> add 0xdead.beefp-16 0x.021524111p+4
Type is Real.
Evaluation:
add 0.8698386510368437 0.13016134896315634
--> 1.0.

Church numerals:

> type CNat = forall a. (a -> a) -> a -> a
CNat := forall a. (a -> a) -> a -> a.
> let cnat2int = \n:CNat. n [Int] (\x:Int. addInt x 1) 0
cnat2int : (forall a. (a -> a) -> a -> a) -> Int.
Evaluation:
\n:CNat. n [Int] (\x:Int. addInt x 1) 0
--> \n:CNat. n [Int] (\x:Int. addInt x 1) 0.
> let csucc = \n:CNat. ?a. \s:a->a. \z:a. s (n [a] s z)
csucc : (forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a).
Evaluation:
\n:CNat. ?a. \s:a -> a. \z:a. s (n [a] s z)
--> \n:CNat. ?a. \s:a -> a. \z:a. s (n [a] s z).
> let cplus = \n:CNat. \m:CNat. ?a. \s:a->a. \z:a. m [a] s (n [a] s z)
cplus : (forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a).
Evaluation:
\n:CNat. \m:CNat. ?a. \s:a -> a. \z:a. m [a] s (n [a] s z)
--> \n:CNat. \m:CNat. ?a. \s:a -> a. \z:a. m [a] s (n [a] s z).
> let c0 = ?a. \s:a->a. \z:a. z
c0 : forall a. (a -> a) -> a -> a.
Evaluation:
?a. \s:a -> a. \z:a. z
--> ?a. \s:a -> a. \z:a. z.
> let c1 = ?a. \s:a->a. \z:a. s z
c1 : forall a. (a -> a) -> a -> a.
Evaluation:
?a. \s:a -> a. \z:a. s z
--> ?a. \s:a -> a. \z:a. s z.
> cnat2int (csucc c0)
Type is Int.
Evaluation:
cnat2int (csucc c0)
...
--> 1.
> cnat2int (cplus c1 c1)
Type is Int.
Evaluation:
cnat2int (cplus c1 c1)
...
--> 2.

Translation from System Fsub to System F:

$ stack exec SystemFsub-repl
This is System Fsub REPL.
Press Ctrl-D to exit.
> translate (\f:Int->Real. f 1) negateReal
[System Fsub] Type is Real.
Translation to System F: (\f:Int -> Real. f 1) ((\f:Real -> Real. \y:Int. f (intToReal y)) negateReal).
[System F] Type is Real.
> translate (?a<:Int->Real. \x:a. x) [Real->Real] negateReal
[System Fsub] Type is Real -> Real.
Translation to System F: (?a. \_coercion:a -> Int -> Real. \x:a. x) [Real -> Real] (\f:Real -> Real. \y:Int. f (intToReal y)) negateReal.
[System F] Type is Real -> Real.
> translate (?a<:Real. \x:a. addReal x) [Int]
[System Fsub] Type is Int -> Real -> Real.
Translation to System F: (?a. \_coercion:a -> Real. \x:a. addReal (_coercion x)) [Int] intToReal.
[System F] Type is Int -> Real -> Real.
> translate (?a. \x:a. x)
[System Fsub] Type is forall a. a -> a.
Translation to System F: ?a. \_coercion:a -> Unit. \x:a. x.
[System F] Type is forall a. (a -> Unit) -> a -> a.

Syntax

type       ::= 'forall' <type variable> '.' type                 -- universal quantified (forall) type
             | 'forall' <type variable> '<:' interType '.' type  -- bounded universal quantified type [Fsub and Finter only]
             | interType
interType  ::= arrowType '&' interType                           -- intersection type [Finter only]
             | arrowType
arrowType  ::= simpleType '->' arrowType                         -- function type
             | simpleType
simpleType ::= 'Int' | 'Real' | 'Bool' | 'Unit'
             | 'Top'                                             -- the universal supertype [Fsub and Finter only]
             | <type variable>
             | '(' type ')'

interTypeList ::= interType ',' interTypeList
                | interType

term       ::= '\' <variable> ':' arrowType '.' term              -- lambda abstraction (function)
             | '?' <type variable> '.' term                       -- type abstraction
             | '?' <type variable> '<:' arrowType '.' term        -- bounded type abstraction [Fsub and Finter only]
             | 'let' <variable> '=' term 'in' term                -- variable binding
             | 'if' term 'then' term 'else' term                  -- conditional
             | 'for' <type variable> 'in' interTypeList '.' term  -- type alternation [Finter only]
             | appTerm
appTerm    ::= appTerm simpleTerm       -- function application
             | appTerm '[' type ']'     -- type application
             | appTerm 'as' arrowType   -- type coercion [Fsub and Finter only]
             | simpleTerm
simpleTerm ::= <integer literal>
             | <floating point literal>
             | 'True' | 'False' | 'unit'
             | <variable>
             | <built-in function>
             | '(' term ')'

Translation from System Fsub to System F

Type:

forall a <: b. ty  -->  forall a. (a -> b) -> ty  (even if b is Top)
Top                -->  Unit

Term:

?a <: b. x  -->  ?a. \_coercion: a -> b. x
x [ty]      -->  x [ty] (<coercion from ty to the bound type>)