3 ms·
> Of course, this leads to type -> type functions which describe dependent and refinement types naturally. could you expand on this? i don't understand how you
by uryga 7y ago
> Of course, this leads to type -> type functions which describe dependent and refinement types naturally.
could you expand on this? i don't understand how you get this from grammars.
(on a side note, i think that dependent types usually mean you can write functions from values to types, not type -> type?)
- wlib 7y agoYes, I mistyped that bit. I meant to say that because types (as a grammar) are values, they can be inputs and outputs of functions. The functions can fill in the hole that dependent/refinement types fill, by taking context into account (the grammars which describe simple types being context free). Type -> Type fill in for type constructors like this infinite list: InfiniteListOf = Type -> Type & InfiniteListOf Type That function just morphs a simple grammar into another grammar. Imagine now if we could calculate something in between: IncrementingInfiniteListFrom = number -> number & IncrementingInfiniteListFrom number+1 That's where the dependent types come in, naturally.