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
From what Andras has told me, it's better to avoid collecting constraints when implementing dependent type systems, as you will end up collecting a large amount of them due to the dependencies at play. It's better to discharge unification problems as soon as possible. :)