Support GADTs

[baronfel]

Submitted by Richard Minerich on 3/21/2014 12:00:00 AM
219 votes on UserVoice prior to migration

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.

Original UserVoice Submission Archived Uservoice Comments

[dsyme]

Note this is hard to implement within the constraints of the .NET type system. We would need to emit reflection code, which feels a bit awkward.

[cloudRoutine]

Could the F# type checker and match expression be extended in a similar manner to the C# GADT implementation? Or is the reflection based type check in the extended switch construct what you were referring to? It seemed similar to the :? type test pattern. If reflection emitted code is unavoidable, would it be possible to store it in a manner similar to delegate binding to amortize the cost? Could the compiler generate IL for a match against a GADT using a combination of an isinst IL check on the TypeDef, TypeRef, or TypeSpec with an IL switch or branches and jmp?

Would it be possible for the compiler to segment the branches of the GADT by the listed type constructors and inline the appropriate corresponding segment method during compilation? Or does that end up constraining the types by too great a degree for it to properly function as a GADT?

Since F# supports subtyping does that mean the typechecker also needs to be extended in the manner described in GADT meet subtyping?

Is it possible to extend the type checker in the manner described in GADTs Meet Their Match in order to provide proper pattern match warnings?

[DemiMarie]

@dsyme What about using boxing and unsafe casts? .NET Core is out of the security game, and I don't see any particular reason that F# needs to generate verifiable code – it just needs to work. So upcast everything to System.Object, and then downcast to the correct type in the match arms.

[dsyme]

@dsyme What about using boxing and unsafe casts?

Pattern matching on a GADTs introduce new type variables into scope. If these are constrained to be uniform representations (i.e. reference types) and you can't do typeof<'T> then the approach you mention will work. That would place a boxing limitation on GADT instantiations however

[DemiMarie]

Another thought: do what Rust does and monomorphize.

On Jan 25, 2018 6:11 AM, "Don Syme" notifications@github.com wrote:

@dsyme https://github.com/dsyme What about using boxing and unsafe casts?

Pattern matching on a GADTs introduce new type variables into scope. If these are constrained to be uniform representations (i.e. reference types) and you can't do typeof<'T> then the approach you mention will work. That would place a boxing limitation on GADT instantiations however

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/fsharp/fslang-suggestions/issues/179#issuecomment-360436358, or mute the thread https://github.com/notifications/unsubscribe-auth/AGGWBwcbCHgdtxhAboR6QRBayBHYfmIAks5tOGFcgaJpZM4Kbo1- .

[krauthaufen]

Wouldn't it be possible to use something like the visitor-pattern behind the scenes when matching on gadts? This should be able to extract the missing type arguments via virtual dispatch.

type GADT =
    | C<'a> of 'a

could be translated to something like:

type C() = 
    inherit GADT()
    abstract member Visit : CVisitor<'r> -> 'r

and C<'a>(item : 'a) =
    inherit C()
    member x.Item = item
    override x.Visit v = v.Accept x

and CVisitor<'r> =
    abstract member Accept : C<'a> -> 'r

That way no reflection code would be needed and all matches would just need to create object-expressions implementing the visitor. That's our current workaround in many projects atm. but as you see it involves a lot of boilerplate that could be generated automatically.

[krauthaufen]

I actually found a similar idea here by Eirik Tsarpalis: http://www.fssnip.net/mp/title/An-attempt-at-encoding-GADTs

However my approach does not require the current code for case-distinction to be changed but only affects the body for certain match-cases (the ones having existential type arguments). Arguably the thing would need to be a little more complicated when supporting when clauses but nonetheless it should be possible. Cheers

[Kazark]

When you are using a (pure data) DSL style for your development (for example an example, see Matt Parson's Three Layer Cake), this is extremely useful. Though the example I referenced was in Haskell, this is my preferred style for F# apps, and overall have found it fairly effective (though it does butt me up against some of the limitations of the language). The concept is this: when you write a (data) DSL, you encode your effects as data. Some effects you might want to encode as needing to perform, without handling any kind of response. However, if you run queries or anything RPC, or other such things, you hit request/response semantics. In this case, you want to be able to encode that data of the request, and couple it with the type of the response (as a phantom type). However typically, in a segment of code, you would express your request effects together in one discriminated union; and so, you need an ability to add a phantom type differently per union case. Rather than making up F# syntax, I will give a small Haskell example:

data Check a where
  FindExe :: KnownExe -> Check (Maybe FilePath)
  ChocoList :: FilePath -> Check [InstalledProgramAndVersion]
  GitConfigCheck :: FilePath -> GitConfigCommand -> Check (Maybe String)

However, to make really good use of this, you also need rank-2 types, which I will describe there.

Currently my workaround is to couple a handler function with every union case, and write out a very rote functor instance e.g.:

type Qry<'a> =
  | GetEnvVar of string*(string -> 'a)
  /// Pure query corresponding to System.Environment.GetFolderPath
  | GetSpecialFolderPath of Environment.SpecialFolder*(AbsPath->'a)
with
  member self.Map (f : 'a -> 'b) : Qry<'b> =
    match self with
    | GetEnvVar (x, handle) -> GetEnvVar (x, handle >> f)
    | GetSpecialFolderPath (x, handle) -> GetSpecialFolderPath (x, handle >> f)
  static member inline map (f : ^a -> ^b, x : Qry< ^a>) : Qry< ^b> =
    x.Map f

This works, but every time you need to add a new union case, you have to change the rote functor instance; and, moreover, this gives you no way to truly represent the idea of the request by itself, but continually couples it to handler code; which has the same negative impact as any other kind of coupling, reducing orthogonality, etc.

[krauthaufen]

Hi all, I don't really see why implementing GADTs requires higher-rank types. My previous suggestion can deal with all cases I can think of and only requires the code-generation for matches/union types to be changed. It is also relatively c# accessible. No reflection, no higher kinded types, just exploiting the one thing OOP can actually do (virtual dispatch). Sorry for the rant :) Cheers

[MaxWilson]

@krauthaufen sorry to be dense but I can't actually figure out how to write the visitor's accept method without using reflection.

{ new CVisitor<int> with member this.Accept(node: C<'t>) = unbox<int>(node.item) }

How do you do it without reflection?

Edit: the second approach you posted, from Eirik Tsarpalis, works great for my scenario. I'm just curious about what you're suggesting in your first comment.

[krauthaufen]

Hey, of course your visitor needs to be able to deal with existential type-arguments. So essentially you cannot know anything about 't (except for constraints) in your Accept implementation.

In lots of cases information about the actual 't is not really required. Consider:

namespace rec Things

// type A =
//    | Array<'a> of 'a[]
//    | Nothing

type IAVisitor<'a> =
    abstract AcceptArray : 'b[] -> 'a
    abstract AcceptNothing : unit -> 'a

[<AbstractClass>]
type A() = 
    abstract Visit : IAVisitor<'r> -> 'r

type Array<'a>(value : 'a[]) =
    inherit A()
    member x.Value = value
    overide x.Visit v = v.AcceptArray(value)

type Nothing() =
    inherit A()
    override x.Visit v = v.AcceptNothing()

type LengthVisitor() =
    interface IAVisitor<int> with
       // here 'a could be any type, but some things like array-lengths may still be possible to get.
       member x.AcceptArray(a : 'a[]) = a.Length 
       member x.AcceptNothing() = 0

[serefarikan]

In case anybody arrives at this issue after looking for a way to make use of GADT's in F#, this talk provides a really nice discussion of the topic, which helps by providing a context for some of the comments in this issue : https://skillsmatter.com/skillscasts/13176-f-sharpunctional-londoners

[serefarikan]

@Kazark may I ask how your approach matches that of Haskell in terms of accessing the actual value wrapped in Qry ? As far as I can see, you can construct any Qry from a Qry using the handler function approach (T -> R) you're providing in the case constructor, but then your R value is 'stuck' in Qry isn't it?

You'd have to pattern match and write all the pattern matching cases to get the R value out, right? I'm trying to understand how one could use your approach from a call site. Different effects my return different types so you'd have to have an exhaustive match for each effect (case constructor) return type in this approach, to use the actual value returned from the effect. I may be a bit confused here :)

[Kazark]

@serefarikan my approach is not a substitute for GADTs; it's a workaround for a particular usecase.

[serefarikan]

@Kazark thanks, much appreciated. Your approach comes pretty close to achieving a key benefit of GADTs, enabling different case constructors to produce different parameterisations of a generic type. Thanks for clarifying your use case.

[dsyme]

Closing this as it requires a change to the .NET CLR and we are not looking to progress that.

Note this is hard to implement within the constraints of the .NET type system. We would need to emit reflection code, which feels a bit awkward.

[DemiMarie]

Closing this as it requires a change to the .NET CLR and we are not looking to progress that.

Aren’t there workarounds for this? One can do pretty much anything with unsafe casts, unsafe unions, and either boxing or monomorphization. Interop with other .NET languages will be nonexistent but that is not really a blocker.

[vzarytovskii]

Closing this as it requires a change to the .NET CLR and we are not looking to progress that.

Aren’t there workarounds for this? One can do pretty much anything with unsafe casts, unsafe unions, and either boxing or monomorphization. Interop with other .NET languages will be nonexistent but that is not really a blocker.

There are certainly ways of emulating those, but proper implementation would require support from runtime.

[DemiMarie]

Closing this as it requires a change to the .NET CLR and we are not looking to progress that.

Aren’t there workarounds for this? One can do pretty much anything with unsafe casts, unsafe unions, and either boxing or monomorphization. Interop with other .NET languages will be nonexistent but that is not really a blocker.

There are certainly ways of emulating those, but proper implementation would require support from runtime.

How would a proper implementation differ from the emulation? The emulation I am describing uses no reflection, just unsafe casts that disappear from JIT-compiled code.