Conversation

Max Desiatov 🇺🇦 🌻🔥
@maxdesiatov
I only wanted to learn how (dependent) type systems work, but ended up prototyping my own programming language inspired by
@SwiftLang
and
@idrislang
. It currently only supports basic expressions and type inference, but may become more useful in the future
Quote Tweet
Kara
@KaraLangOrg
·
Hello, world! Star and watch our repository on GitHub for imminent updates github.com/kara-lang/Kara
1
14
Max Desiatov 🇺🇦 🌻🔥
@maxdesiatov
Why dependent types? If all works well, I want to prevent out of bounds access in arrays at compile-time. That is, this will not type check in (a future version of)
@KaraLangOrg
: let a1 = [1,2,3] a1[3] // type error, out of bounds let a2 = [4,5,6] (a1 + a2)[6] // type error, OOB
3
1
Brendan Zabarauskas
@brendanzab
It'd come down to the types you give your indexing and concatenation functions. Eg: _[_] : {n} {A} -> Array n A -> Fin n -> A _+_ : {n m} {A} -> Array n A -> Array m A -> Array (n + m) A
1
1
Brendan Zabarauskas
@brendanzab
At the point where you want to check `(a1 + a2)[6]`, the addition in the `_+_` reduces definitionally, so `a1 + a2` is of type `Array 6 Int`. And then you'd get a type error saying that you can't make a `Fin 6` using the numeric literal `6`.
1
2
Brendan Zabarauskas
@brendanzab
A difficult part of getting these type systems to work is implementing efficient (and correct) conversion checking for open terms, and this shows how to do it in a nice, up-to-date way. Highly recommended!
1
Brendan Zabarauskas
@brendanzab
It walks though using normalisation-by-evaluation using de Bruijn levels and indices, which is pretty important for performance (cuts down on tree traversals, and increases laziness), and also shows how to implement pattern unification in a way that works well in these settings.
1
1