I suggest we ...

Add support for GADTs

Generalized Algebraic Data Types essentially extend standard union types to allow different generic instantiations when defined recursively.

You can see a simple explanation of how they work in haskell here: https://en.wikibooks.org/wiki/Haskell/GADT

They open the door to such fantastic type safe data structures as heterogeneous lists and so can vastly improve type safety within the language.

219 votes
Vote
Sign in
(thinking…)
Password icon
Signed in as (Sign out)
You have left! (?) (thinking…)
Richard Minerich shared this idea  ·   ·  Flag idea as inappropriate…  ·  Admin →

5 comments

Sign in
(thinking…)
Password icon
Signed in as (Sign out)
Submitting...
  • George Pollard commented  ·   ·  Flag as inappropriate

    Regarding Don's comment: if matching over GADTs were restricted to occur in the same module, could it be compiled down to a virtual method (with an exported function that invokes it)?

  • Don Syme commented  ·   ·  Flag as inappropriate

    A major consideration is that GADTs are difficult to compile to .NET IL efficiently. Specifically, it is not possible to recover an existentially-hidden type variable except via virtual dispatch. For example

    type C

    type D<T> : C

    If we have a C, a GADT implementation may "know" that for certain cases T has certain values, or decomposes in certain ways. But you can't implement this in .NET IL generics - you have to use reflection to recover the value of T and instantiate the branch code with a specific value. Russo and Kennedy had a proposal for what to do about this for C#.

    This is a significant blocking factor for adding this to F# - GADT code would need reflection and would be less efficient.

F# Language

Feedback and Knowledge Base