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
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
Show replies
Max Desiatov 🇺🇦 🌻🔥
@maxdesiatov
Replying to
@brendanzab
@moonriseTK
and
@KaraLangOrg
Thanks, been watching that repository already. I'm still at a stage of implementing dependent pattern matching, and distracted by the dev tools situation. As I start playing w/ more code, I need syntax highlighting and language server with proper error messages for my language 🙈
1
1
Brendan Zabarauskas
@brendanzab
Ah cool, sorry! Yeah I see you've done a good job of getting things hooked up. Thought I'd give it a spruik it based on what I'd seen of the type checking and evaluation implementation. But I understand it's a WIP.
1
Show replies