Verity Scheel

I’m wondering if something like what ST does would work here? Universally-quantified regions to encapsulate the values at the type level so they only appear in a certain scope. (I...

Hi! Thanks for the interest. I don't think this particular library will be suitable for a JS/TS API, since the datatypes are so different from what they would look like...

Known bugs ATM: - [x] `SetSelection` does not seem to work on deeper selections - [x] Typing `(Lam : Pi) App` with `(Pi -> Lam) App` might result in wrong...

Generalize everything! - [ ] Extensible locations - [ ] Let Oxpr take outside annotations too (monoidal?) - [ ] Let typechecking occur in any bind+applicative (hmm I'm not entirely...

https://github.com/dhall-lang/dhall-haskell/pull/612#issuecomment-425982859 http://www.haskellforall.com/2017/09/type-driven-strictness.html

- [x] Need to move normalization into its own file. - [x] Break apart normalization into various passes. - [ ] Break apart typechecking into its cases, give names to...

what we need is ✨ _universe polymorphism_ ✨

Unicode casing is a little complicated, because there are both simple (codepoint-by-codepoint) and [full](https://www.unicode.org/Public/13.0.0/ucd/SpecialCasing.txt) algorithms (which may replace single codepoints by multiple codepoints), and there's four different case conversions available:...

Keys are sorted according to `Ord` instance in Haskell :) (for unions, union literals, records, and record literals) In my [dhall-purescript](https://github.com/MonoidMusician/dhall-purescript) project, I essentially have forms of normalization that _do_...

The problem with the return-type primitive is that it would require evaluation to depend on type inference, which would be a large change to how the language works. However, I'm...