Hacker News Reader

Comment by def-lkb | Hacker News Reader

Indeed. GADTs provide type equalities and existentials. This example involves neither, only sub-typing (which is quite strong and interesting in Typescript)

View on HN

Something 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_m...

An 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....

Reply on news.ycombinator.com