Hacker News Reader

Comment by whateveracct | Hacker News Reader

Once you understand their basics, GADTs are as easy to use as any other mainstream language feature. I wonder if any mainstream language will meaningfully have them soon. Not technically (many do) but meaningfully. Lightweight syntax and fully-powered pattern matching.

View on HN

OCaml already does. Some good examples -

JSON GADT : https://github.com/OCamlPro/ocplib-json-typed/blob/0d9e9cde7...

Mirage/repr, uses GADT's for representing OCaml types as runtime values which are used for implementing dynamic polymorphism - https://github.com/mirage/repr/blob/main/src/repr/type.ml

I count OCaml as "mainstream" as Haskell ;) it's one of the good ones

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)
    );

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

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

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

Um that's just an ADT, not a GADT...

Haxe does.

Not that Haxe is mainstream, but it does target mainstream languages.

Reply on news.ycombinator.com