Commit 5459fde8 authored by Nicolas Lenz's avatar Nicolas Lenz

Low-level languages

parent b5e28a7b
......@@ -144,7 +144,7 @@ Implement a algebraic compiler using `megaparsec` for parsing in Haskell and lat
Katrin code ist first parsed into a normal abstract syntax tree. This is then transferred into KatrinLite, which is essentially a desugared version of Katrin. KatrinLite is then translated to KatrinCore, which is a basic representation based on the lambda calculus without any advanced features. This is then compiled to an external intermediate language which can be used with a external compiler to produce machine code.
- [Idris2](https://github.com/edwinb/Idris2) uses »quantitative type theory« as base for the core language, look into that
- [System F](https://en.wikipedia.org/wiki/System_F) (extended for GHC with GADTs to System F~c~)
- GHC uses [System F](https://en.wikipedia.org/wiki/System_F) as intermediate representation, extended with GADTs to System F~c~
- Type-checking on KatrinLite or KatrinCore?
- Optimizations on KatrinLite or KatrinCore or both? KatrinCore should be optimal for this, while some simplifications of course need to be performed when compiling Lite to Core.
- Is using two intermediate languages even helpful?
......@@ -154,11 +154,11 @@ Katrin code ist first parsed into a normal abstract syntax tree. This is then tr
- Idris2 also does this: They have a intermediate (TTImp) and a core language.
- Do we need a runtime system to be linked against? Probably. Look into the Haskell runtime system.
Which intermediate language could be used to produce binaries?
Which intermediate language could be used for the backend to produce binaries?
- [GraalVM](https://en.wikipedia.org/wiki/GraalVM)
- Looks really promising
- Supports JVM and native
- Supports JVM and native images
- Support for mixing with any programming language – being able to use Java, Python etc. libraries could be a *huge* advantage
- C-- (used by GHC)
- Looks kind of obscure and doesn't really seem to be maintained.
......@@ -217,6 +217,31 @@ Debugging needs to be easy and comprehensive.
## Other Interesting Languages
### Low-Level
- [Untyped lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus) (well, duh)
- Recursion not directly possible because of all functions being anonymous
(That is, values can be defined and used later as syntactic sugar: `x=5; x+1` could be modelled as `(λx.x+1)5`, but this doesn't work for recursion or circular dependencies)
- Instead it is modeled via fixed-points: [Fixed-point operator](https://en.wikipedia.org/wiki/Fixed-point_combinator)
Instead of
```
fact = λn. if n == 0 then 1 else n * fact (n-1)
```
:
```
fix = λg. (λx. g (x x)) (λx. g (x x))
fact' = λr. λn. if n == 0 then 1 else n * r (n-1)
fact = fix fact'
```
- [Simply-typed lambda calculus](https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus)
- Note that this isn't turing complete as there's no recursion
- No recursion because of impossibility to assign type to fixed-point-operator
- [System F](https://en.wikipedia.org/wiki/System_F)
- [SKI combinator calculus](https://en.wikipedia.org/wiki/SKI_combinator_calculus)
### High-Level
- Haskell
- Idris
- Agda
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment