Conversation

Nov 16, 2021

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

· Nov 11, 2021

Hello, world! Star and watch our repository on GitHub for imminent updates github.com/kara-lang/Kara

Max Desiatov

@maxdesiatov

Nov 16, 2021

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

Tanishq Kancharla (tk)

@moonriseTK

Nov 16, 2021

p cool!

@brendanzab

do you happen to know anything about how you would do this, im curious myself

Replying to

and

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

12:00 PM · Nov 16, 2021Twitter Web App

Replying to

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`.

Brendan Zabarauskas

@brendanzab

Nov 16, 2021

For more information on making these kinds of type systems, I'd highly recommend checking out github.com/AndrasKovacs/e :)

github.com

GitHub - AndrasKovacs/elaboration-zoo: Minimal implementations for dependent type checking and...

Minimal implementations for dependent type checking and elaboration - GitHub - AndrasKovacs/elaboration-zoo: Minimal implementations for dependent type checking and elaboration

Show replies