25 ms·
Typescript, as a counterexample, doesn't need GADTs because it has first-class union support + nice type filtering. There's a bit of manual tagging that's neede
by rtpg 5y ago
Typescript, as a counterexample, doesn't need GADTs because it has first-class union support + nice type filtering. There's a bit of manual tagging that's needed but the ergonomics are both easy to understand and more flexible (not to mention supporting even other usage patterns).
type Term = {kind: 'lit', value: number} | {kind: 'pair', left: Term, right: Term};
function pair(left: Term, right: Term): Term & {kind: 'pair'} {
return {kind: 'pair', left, right};
}
function lit(n: number): Term & {kind: 'lit'} {
return {kind: 'lit', value: n};
}
let t: Term = pair(
pair(lit(1), lit(2)),
lit(3)
);
- lmm 5y agoYour example doesn't show using a type parameter, which is what makes a GADT a GADT. As far as I can see your example is just an ADT.
- def-lkb 5y agoIndeed. GADTs provide type equalities and existentials. This example involves neither, only sub-typing (which is quite strong and interesting in Typescript)
- culturedsystems 5y agoSomething pretty similar to the AST example in another thread can be implemented in Typescript using sub typing (as it happens, trying to do something like that is how I first found out about GADTs). Looking into existential types, I see that one of the things they can be used for is OOP style subtype polymorphism [1]. Are there things you can do with existential types that can't be done with subtyping? [1] https://wiki.haskell.org/Existential_type#Dynamic_dispatch_mechanism_of_OOP https://wiki.haskell.org/Existential_type#Dynamic_dispatch_m...
- lmm 5y agoAn ADT is a "closed" type like an enum, which then enables other features that you can't implement for OO-style "open" subtyping (e.g. pattern matching). You can encode that in a traditional-OO language with the visitor pattern, but it's very cumbersome to work with in practice. The other subtle thing with GADTs is that the type information must flow back from the matched case to the type parameter: if you match an Ast<R> and get Mul, you know that R=Int. And that part is impossible to do fully in a language that doesn't have higher-kinded types, because you not only need to be able to know that you can pass an Int where an R was expected, but also that you can pass an Ast<Int> where an Ast<R> is expected, or return a List<Int> where a List<R> is expected, or....
- deleted 5y ago[deleted]
- ebingdom 5y agoUm that's just an ADT, not a GADT...