search

escalier-lang / escalier-next

Improved type safety with tight TypeScript interop
https://escalier-lang.github.io/escalier-next/
MIT License
14 stars 0 forks source link

Dependent types #118

Open kevinbarabash opened 10 months ago

kevinbarabash commented 10 months ago 
let push = fn <T, N: unique type>(vector: Vec<T, N>, item: T) -> Vet<T, N + 1>
let pop = fn <T, N: unique type>(vector: Vec<T, N + 1>, item: T) -> Vet<T, N>

Avoid subtraction whenever possible.

kevinbarabash commented 9 months ago

Here's a tutorial that looks like it may be useful: https://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/