You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
53 lines
998 B
53 lines
998 B
# Language syntax
|
|
|
|
### Abstractions:
|
|
```
|
|
\x:T.e
|
|
```
|
|
Where `x` is an identifier, `T` a type, and `e` an expression
|
|
|
|
### Aplication:
|
|
```
|
|
lhs rhs
|
|
```
|
|
Where `lhs` and `rhs` are expressions
|
|
|
|
### Variable:
|
|
```
|
|
x
|
|
```
|
|
Where `x` is an identifier
|
|
|
|
### Constants:
|
|
```
|
|
n
|
|
```
|
|
where n is an number
|
|
|
|
or
|
|
```
|
|
true
|
|
```
|
|
|
|
or
|
|
```
|
|
false
|
|
```
|
|
|
|
## Types
|
|
|
|
The language has the primitive types `Bool` and `Nat`, and arrow types
|
|
of the form `T1 -> T2`, where multiple of these can be composed, and
|
|
parentesis can be used to specify associativity, ex: `(Nat -> Nat) -> Nat -> Nat`
|
|
|
|
# Using the repl
|
|
|
|
When entering a valid expression into the repl, it will be type checked, and if well typed,
|
|
its beta reduced form and type is printed.
|
|
|
|
The repl offers additional commands starting with `:`, the following commands are availaibe
|
|
|
|
- `:t expr`: get the type of `expr`, but do not beta reduce
|
|
- `:ctx ident : T`: add a variable identfied by `ident` of type `T` to the type checking context,
|
|
arrow types need to be in parentesis
|