README.md 886 Bytes
Newer Older
Nicolas Lenz's avatar
Init    
Nicolas Lenz committed
1
# Type Systems
Nicolas Lenz's avatar
Nicolas Lenz committed
2

Nicolas Lenz's avatar
Init    
Nicolas Lenz committed
3
4
Testing out various type systems in Haskell.

Nicolas Lenz's avatar
Nicolas Lenz committed
5
Currently allows for primitive expressions to be evaluated and typeckecked allowing for "true", "false", "if E then E else E", "0", "succ E", "pred E", "isZero E" and "(E)" where E is an expression.
Nicolas Lenz's avatar
Init    
Nicolas Lenz committed
6

Nicolas Lenz's avatar
Nicolas Lenz committed
7
8
Take a look at my language [Lightfold](https://git.eisfunke.com/software/lightfold/lightfold) for an interpreter and typechecker for a more elaborate language.

Nicolas Lenz's avatar
Init    
Nicolas Lenz committed
9
10
11
12
13
14
15
Run with `stack run` to open the test shell interface. Enter an expression in the shell to see it parsed and evaluated.

E.g.

```
expr> if (isZero (succ 0)) then succ 0 else pred (succ 0)
Term: If (IsZero (Succ Zero)) (Succ Zero) (Pred (Succ Zero))
Nicolas Lenz's avatar
Nicolas Lenz committed
16
Type: Just TNat
Nicolas Lenz's avatar
Init    
Nicolas Lenz committed
17
Result: Just Zero
Nicolas Lenz's avatar
Nicolas Lenz committed
18
19
20
21
22
23
24
25
expr> isZero (succ 0)
Term: IsZero (Succ Zero)
Type: Just TBool
Result: Just EFalse
expr> isZero (succ true)
Term: IsZero (Succ ETrue)
Type: Nothing
Result: Just EFalse
Nicolas Lenz's avatar
Init    
Nicolas Lenz committed
26
27
expr>
```