3 ms·

Internally, the Idris2 compiler uses deBruijn numbering for its terms, which is tricky to get right once you start trying to manipulate terms. To help with this

by dunham 4y ago

Internally, the Idris2 compiler uses deBruijn numbering for its terms, which is tricky to get right once you start trying to manipulate terms. To help with this, it keeps a list of the names corresponding to the deBruijn indices at the type level. The type checker catches mistakes as you write code to manipulate them (inserting names, removing names, or renaming things). I ran through some exercises teaching this technique[1]. My take-away as a beginner was that it was a pain to make the compiler happy and my code that the compiler didn't like was actually wrong. I remember reading someone had written a functional red-black tree (with proof of correctness leveraging dependent types) and said the delete algorithm naturally followed from the types. That has was not my experience (delete wasn't immediately obvious to me), but I need to find some time to give it another go. The Idris2 docs have an example of a lambda expression interpreter[2] whose terms have a vector of the types in the environment as a type parameter (erased at runtime), to ensure everything is type safe in the resulting interpreter. Typescript has added some bits of dependent typing. For example, asserting a function returns true if the argument has type X, that a function throws if the argument is falsy, and I think type level string manipulation. They are fairly pragmatic, it's not a research language, so I presume that specific functionality is useful to a lot of people. I've used it a little bit of it to help the type checker infer non-null after my assert function was called. All of that said, I think people are still exploring how dependent types can be used in practice. [1]: https://github.com/edwinb/SPLV20/blob/master/Code/Lecture2/Exercises.txt https://github.com/edwinb/SPLV20/blob/master/Code/Lecture2/E... [2]: https://idris2.readthedocs.io/en/latest/tutorial/interp.html https://idris2.readthedocs.io/en/latest/tutorial/interp.html There is a copy of #1 at github.com/dunhamsteve/SPLV20 that is updated to work with the latest Idris2.

wk_end 4y ago
TypeScript does not have dependent types. It has type-level constants and surprisingly powerful type manipulation facilities, including string manipulation on string type constants. But there's no way to operate on types at the "dynamic" expression level - they're deliberately erased, to the point that transforming TypeScript to JavaScript is almost trivial. For example, take the very first example of a dependent type in the Idris tutorial - a function `isSingleton` that consumes a `Bool` and produces `Nat` if you give it `True` and `List Nat` if you give it `False`; it then uses `isSingleton` as part of the type of `mkSingle`, a function that consumes a `Bool` called `x` and produces an `isSingleton x` - that is, a `Nat` if `x` is `True` and a `List Nat` if `x` is `False`. There's no way to write this in TypeScript. You could have `isSingleton` return dynamic constructors instead, but you can't use that `isSingleton` as part of the type of `mkSingle` to generate a return type. Your `mkSingle` would be stuck with the signature `(x: boolean): number | number[]`; which branch of the return type you end up with depends on `x`, but there's no way to make TypeScript properly understand the connection.
zasdffaa 4y ago
> Internally, the Idris2 compiler uses deBruijn numbering for its terms, which is tricky to get right once you start trying to manipulate terms I'm lost. Why does it use them; what does it get from doing so? Also if it's internal why would you as a language user (vs implementer) ever encounter them?

by dunham 4y ago

wk_end 4y ago

TypeScript does not have dependent types. It has type-level constants and surprisingly powerful type manipulation facilities, including string manipulation on string type constants. But there's no way to operate on types at the "dynamic" expression level - they're deliberately erased, to the point that transforming TypeScript to JavaScript is almost trivial. For example, take the very first example of a dependent type in the Idris tutorial - a function `isSingleton` that consumes a `Bool` and produces `Nat` if you give it `True` and `List Nat` if you give it `False`; it then uses `isSingleton` as part of the type of `mkSingle`, a function that consumes a `Bool` called `x` and produces an `isSingleton x` - that is, a `Nat` if `x` is `True` and a `List Nat` if `x` is `False`. There's no way to write this in TypeScript. You could have `isSingleton` return dynamic constructors instead, but you can't use that `isSingleton` as part of the type of `mkSingle` to generate a return type. Your `mkSingle` would be stuck with the signature `(x: boolean): number | number[]`; which branch of the return type you end up with depends on `x`, but there's no way to make TypeScript properly understand the connection.

zasdffaa 4y ago

> Internally, the Idris2 compiler uses deBruijn numbering for its terms, which is tricky to get right once you start trying to manipulate terms I'm lost. Why does it use them; what does it get from doing so? Also if it's internal why would you as a language user (vs implementer) ever encounter them?