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
Max Desiatov 🇺🇦 🌻🔥
@maxdesiatov
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
Max Desiatov 🇺🇦 🌻🔥
@maxdesiatov
Replying to
@brendanzab
and
@moonriseTK
Thanks! Code I posted here in the thread will not at work at all right now, example snippets are aspirational 😅. The only way to sanely interact with it is through test cases. Generic types are not supported yet, and it does only simple evaluation in type signatures. V early WIP
1