Lambda the Ultimate

Instead of "semantically simpler" I probably should have said "closer to the semantics", which is what I meant. I also didn't give much time to the use of "where" (or its omission!). I think Haskell's syntax is slightly confusing. For example, I would scratch my head at this for a moment:

    data Foo a b where
        foo :: b -> a -> Foo b a

I would scratch my head at this for a moment:


data Foo a b where
foo :: b -> a -> Foo b a


Yes that's perverse naming.

That's not a GADT, although it's using GADT style syntax. (I'll overlook another syntax error.) Compare


data Foo a b = Foo a b -- equiv to your Foo a b
data Bar a b = Bar b a


You can use the type constructor or the data constructor partially applied. Perhaps there's reasons to want the type constructor partially applied to the type of the data constructor's second arg.

Interesting. It doesn't work like I thought. Are the type parameters to the (syntactic) GADT even in scope, then?

data Foo x y where
    Foo :: a -> b -> Foo a b -- Is x in scope here?

One thing I find appealing about the guard syntax is that it seems to unify the two syntaxes:

data Foo a b
    foo a b -- Ordinary ADT

data Foo a b
    foo a b | a ~ Int -- GADT

An ADT is just a GADT with no guard clauses.

Are the type parameters to the (syntactic) GADT even in scope, then?

No: as the User Guide says, "Named arguments are entirely optional." This is the same decl:


data Foo :: * -> * -> * where ...


So if I unpeel your O.P. to be asking why are there two Foos, rather than to be proposing some different syntax:
* One is declaring type constructor Foo, the other is using it.
* Does it need to be so verbose? Probably not: the syntax has been grafted on to H98 which didn't have GADTs.

So data Foo a b (whatever follows it) says:
* I am declaring a new type constructor Foo.
* It has two type parameters.
* It constructs a data type whose type parameters are therefore injective.

Contrast type Baz a b (type synonym) or type family Quux a b which are lexically indistinguishable when they appear in types, but are not injective.

Nevertheless, the named type parameters might be doing something useful in the Brave New World of dependent Haskell. With PolyKinds you can go


data Gosh k (a :: k) where ...


I really think you should stop thinking of anything in GADTs as being type-level guards. They're a species of constraints. (If all else fails you could read the User Guide to find out why.) Pattern matching on a GADT constructor says: within scope of this match, the matched variable is of type Int. It does not say: only match this pattern if the argument is an Int.

I feel that your answers are very hung up on the details of the wording of the Haskell reference, rather than the underlying concepts and the fact that several different syntaxes and naming schemes have been proposed over time (starting at the introduction of existential variables in algebraic datatypes by Läufer and Odersky, 1992).

This paragraph in particular is somewhat perplexing:

I really think you should stop thinking of anything in GADTs as being type-level guards. They're a species of constraints. (If all else fails you could read the User Guide to find out why.) Pattern matching on a GADT constructor says: within scope of this match, the matched variable is of type Int. It does not say: only match this pattern if the argument is an Int.

GADTs have been repeatedly called Guarded Algebraic Datatypes, so using the word "guard" seems fairly sensible to me. The fact that the usage is not exactly the same as what "guards" mean in the context of pattern matching clauses in Haskell is unfortunate, but we have plenty of name conflicts in this way ("functors" has many meaning). Calling these constraints instead of guards is also fine (although it would have felt strange to people working on type-inference in GADTs, where constraints meant type-inference constraints).

Finally, I am not sure your distinction between "within the scope of this match" and "only match if ..." is meaningful. Both meanings result in exactly the same pragmatics (we want to hide clauses which would add incoherent constraints to the environment), and switching between the two fairly-close point of view can be useful.

My general impression is that Matt's syntactic musing are, in the abstract, very sensible. (`where` has been proposed as a keyword by the work of Andrew Kennedy and co-authors on GADTs in C#, and is bound to occur in Rust's flavor of GADTs when they generalize trait costraints.) It's perfectly reasonable to explain that the Haskell Reference presentation takes a different view on how to present GADTs, but I wouldn't draw certainty from those differences.

I feel that your answers are very hung up on the details of the wording of the Haskell reference,

because Matt is asking about Haskell (look at the first sentence of the O.P.). And in Haskell the G stands for Generalized.

Perhaps it's different in C# or Rust. I wasn't talking about them. And perhaps "guard" means something different (or isn't a term of art) in those languages.

In Haskell GADTs are desugarred to constraints -- I gave examples. And I do mean type-inference constraints. That's why the examples used constraint syntax.

With a guard in Haskell I can put several equations with the same pattern, different guards:

f (Just x) | x == 0 = ...
f (Just x) | x > 0 = ...
f (Just x) | x < 0 = ...

There's nothing corresponding to multiple case branches for GADTs (in Haskell). That's why I think it's not helpful to think in terms of "guards".

EDIT: I mean nothing like (to borrow Matt's example):

data Foo a b
    Foo a b | a ~ Int
    Foo a b | a ~ Bool

In constructing a type Foo you don't inspect the type of the argument then choose the data constructor. Rather, you choose the data constructor and that insists you supply an Int as argument. Similarly in deconstructing, you pattern match on the bare data constructor, and that delivers a guarantee the argument is bound to Int.

several different syntaxes and naming schemes have been proposed over time (starting at the introduction of existential variables ...

To bikeshed: existentially quantified fields are not quite the same thing as Matt is asking about. It's terrific that Haskell's GADT syntax can express them too. (That is, as well as 'equality-qualified types', to use another term.) In

data Baz a b where
    Baz :: Show c => Int -> b -> c -> Baz Int b

type c is existentially quantified because it doesn't appear in the result type Baz Int b. So I'm struggling to think of c as being 'guarded'. Whereas I can see that GADTs generalise ADTs with a uniform syntax for disparate extensions.

I concede your point that existentials are another generalization of ADTs that are not "guards", but I'm not worried about the name. I'm interested in learning new advantages / disadvantages of this scheme. Your example would be:

data Baz a b 
    baz a b c |  a ~ Int, Show c

Edit: But just to make sure we're on the same page - the motivation for my calling them guards is the semantics of Baz as the fixpoint of an operator. In that operator, we will find equality tests comparing parameter a to Int and it seems reasonable to me that we call this a guard (I don't think I'm confused about constructor vs. types or about constraints vs. branching).

But just to make sure we're on the same page ...

hmm, nearly

the semantics of Baz as the fixpoint of an operator. In that operator, ...

Do you mean Baz the data constructor? Then could you manage to spell it starting upper case in your code please. Data constructors are rather more than operators.

we will find equality tests comparing parameter a to Int ...

An operator applies equality tests at run time. Requiring a to be Int applies at compile time. If the compiler can't prove that (and/or can't find a Show instance for c), then we don't just get an equality test that comes out False, we get the program rejected as ill-typed. That's in Haskell/statically typed languages. Dynamically typed languages might be different.

and it seems reasonable to me that we call this a guard

Your code is very close to being legal Haskell. I don't see what using guard syntax (in a place where it's illegal) is gaining you. If you used constraint syntax:
* the User Guide would make sense
* the error messages would make sense
* you could follow the academic papers GADTs aka '(equality-)qualified types'

data Baz :: * -> * -> * where
    Baz :: (a ~ Int, Show c) => a -> b -> c -> Baz a b

I meant semantically the type is something like this:

type Baz = Λt. μx. ∀abc. a → b → c → (t = Int)? (Show c)? {baz : (a, b, c)}

The question mark is a binary guard operator that evaluates to the empty type if the predicate doesn't match or the RHS if it idoes. And probably that should be a nu instead of a mu because of laziness. The context for my question is the design of my own language, which is why all of the not-quite-Haskell keeps creeping in. Edit: cleaned up my bungled type some. Maybe I fixed it.

Your are describing the type of a constructor here, not the type of the constructed data; in particular your (mu x.) does not work to correctly allow recursive occurrences.

A standard GADT encoding would be to turn

type foo a b =
| Bar : Show c => b -> foo b c -> foo Int b
| ...

into

foo = mu t. Lam a b .
  ((exists c. (a = Int, Show c) ? (b * foo b c)) + ...)

but you could use a more regular/systematic encoding to have

foo = mu t. Lam a b.
  ((exists b' c. (a = Int, b = b', Show c) ? (b' * foo b' c)) + ...)

(All types used in the constructor types are existentially quantified, and there is one equality constraint for each type parameter.)

I was closer before my edit :).

An ADT is just a GADT with no guard clauses.

You could (again) just look at the User Guide.

"It is permitted to declare an ordinary algebraic data type using GADT-style syntax. What makes a GADT into a GADT is not the syntax, but rather the presence of data constructors whose result type is not just T a b."

So the type parameters are constrained, as specified in the type of the data constructor.


Foo :: Int -> b -> Foo Int b -- desugars to
Foo :: (a ~ Int) => a -> b -> Foo a b

Classy :: (Show a, Typeable b) => a -> b -> Fancy a b


Note also "the presence of data constructors whose ..." doesn't mean that all data constructors within a GADT need to something other than plain T a b: you could have a mix.

I should think through some bigger examples and see if the other syntax becomes cumbersome.

But thanks to you and AntC for responding. The reason for my question was a concern that I was missing a better reason, not to criticize the design of Haskell. My knowledge of PL theory has holes, so I need to occasionally check that I haven't lost the plot.

Those features are also open. I think you'd have to be careful specifying what your rule is to ensure non-overlapping patterns at link.

To me it seems like the abusing-types-for-meta-programming features in Haskell are kind of ugly, including GADTs with that question mark operator. But one thing it would help is if I understood the rationale - why is it OK to do type comparisons in a GADT "guard" but not OK to do if-then-else on types in a general setting?

why is it OK to do type comparisons in a GADT "guard" but not OK to do if-then-else on types in a general setting?

In dynamically typed languages you might. And then you might get a type error at run-time.

Haskell is statically typed, with the mantra 'well-typed programs can't go wrong'.

So (I'll say it again) taking a GADT constraint as a "guard" is confusing your thinking (in Haskell). Applying a GADT constructor in a term raises a wanted constraint: this argument must be Int. It doesn't inspect the argument and do one thing if it's Int, a different thing if it isn't. Haskell's design is to make type inference complete and decidable. (Although certain celebrated extensions relax that, GADTs isn't one of them.)

If the argument turns out to be provably something other than Int, compilation fails. If the compiler can't prove either way, it'll assume Int, and try to proceed with other type solving.

If the GADT constraint is a class Show c, the -else gets even harder: the compiler can't prove that c isn't in Show. Perhaps there's a distant module with a suitable instance. Type evidence is a constructivist logic.

I think the rationale is something to do with constructive types. You can't ever ask for the negation of a type. But I don't really appreciate why that means what we're doing is a good idea. I'm not talking about "run-time" type inspection or something, but there is conditional guarding on types in the semantics of GADTs. It feels clumsy to me, muddling types as sort-of sets with some kind of meta-data.

I think that's right though, types are sort of sets, and sort of metadata.

I think what types really are, are static proofs (or guarantees) that a value is in a certain set. This guarantee allows us to use overloaded encodings. We have to represent everything as bits (but let's limit ourselves to machine words for simplicity). The same machine word can represent different things depending on the encoding, for example an integer or a float, the actual value represented would be different for the same machine word depending on the selected coding. Static types have to guarantee that coding so that there is no record of the coding in the final program (as that would be a dynamic type). So it comes down to proving that only one encoding is used to access data at a given address (although again this is made more complex by re-use patterns like stacks).

So static types are meta-data in the sense they exist at compile time but get erased, but I would say they are encodings rather than sets of values, but can be considered as constraints on value.

You can assume type equalities on types in a general setting by adding a (a ~ Int) constraint in your environment. Negation is also expressible; even if your language has no surface syntax for "false" as a constraint, you can use a computationall witness ((a ~ Int) => Empty), where Empty is an empty type.

You cannot do an if-then-else due to the constructive nature of type-level evidence: it is not the case that either you can prove (a ~ Int) or you can prove its negation. But you can certainly dispatch over both, writing two terms with each constraint and pairing them. (If we had disjunctions at the level of constraints, we could even assume some form of excluded-middle for some types.)

Three potential criticisms of GADTs:

• The notion of type equality used is very syntactic. One may want something closers to "there exists a bijection between those types", although I'm not convinced it is the right default for a computation-oriented language, or at least equating types that are known to be empty.
• You may want to express subtyping rather than equalities in many scenarios (equalities making things more brittle).
• Expressing functions between types as GADTs is cumbersome, because you have to express them as relations, and write the term-level witnesses for why those relations hold. (A principled way to elide values that are uniquely-determined from their type and make them computationally inexpensive could have solved this part.)

I haven't done a good job of expressing my concerns with GADTs or type classes or type families. I'll try to be marginally more coherent.

Let's start with negation. I understand that we can encode constructive negation, but sometimes it seems we would want classical negation. As an example, consider writing a pretty printer for various types (Haskell's show). Why can't we add a default that prints "<unknown type>" (or, even better "<unknown type X>")? IMO, we should be able to do that; the benefit seems clear. But when you understand type classes as "branching on type", that's a big problem, because code like this can't possibly work:

    foo :: forall a::*. a -> String
    foo = show  -- How do we get an instance of Show here?

The problem to me is that we've conflated the static descriptor of types, which we should be able to inspect and use for meta-programming, with the logical proposition or set denoted by the type.

GADTs should be considered a meta-programming facility for building a datatype that follows a regular (automata sense) blueprint rather than having all recursive invocations the same. It should be parameterized by the meta-data part of types, rather than having those question mark operators as type theoretic equality constraints.

I particularly agree with your criticism of GADTs in the presence of subtyping and I've posted something about that here in the past. But I think it's much harder to fix than just "switching to subtyping constraints" (what would be the type of a 'plus' Term?).

Maybe this hasn't been particularly convincing, either, but thoughts along these lines are why I have a suspicion that the way we use types for meta-programming in e.g. Haskell is wrong.

I think using types for meta programming is fine (although perhaps your criticism is regarding how they are used in Haskell?). I see some flaws in Haskell, like there should be backtracking on instance resolution.

For me the type of a variable is just a piece of metadata (we can have other static compile time metadata too) and we can write logic programs to direct compilation of the program using this metadata.

So whilst I might have problems with the details of how Haskell does this, I don't have a problem with the general idea of writing compile time logic programs. This also relates to proof theory as the program generated by solving the logic program formed by the typeclass instances is the proof.

The type equality constraints would have to be equality, as subtype would be a different constraint?
I suspect I don't really understand your problem here. We should be able to have classical negation in a GADT because they are closed.

I think the major difference between treating types as static descriptors and treating types as logical entities is how type variables are treated.

Can you say more about the specific differences, because I don't really follow you, so I am probably missing something?

I'm just saying that if you view types as static descriptors of values, then one of the possibilities is that you find a descriptor for "type variable". It doesn't work like this in Haskell. A type variable is a type you don't know yet.

What do you mean "a descriptor for a type variable"? Are you talking about runtime dynamic typing?

I'm talking about the difference between treating a type variable as a type to be provided later vs. a type itself. In a static context, a type variable is a type and we should be able to do meta-programming on it, I think. If you have typecase semantics, then you think of the type as a parameter and constraint the context to require typecase information on the variable.

I think a type variable stands for an as yet unknown type, and we can write logic programs with them.

I am not sure how a type variable could be a type? Thats like saying "1 + x = 7" and "x" is a number. Even then I find it hard to even think what that means, as obviously "x" is just a different way of writing "6" even if we consider it a number in some alien writing system?

If you separate the meta-data aspect of types from the logical aspect, then you can have the logical aspect be a parameter, but the meta-data is just a formal symbol. Types can be a local mechanism for lightweight theorem proving and meta-programming rather than some global mechanism that requires a weird linker step.

I must have not had enough coffee today. I agree when you say types can be a local mechanism for lightweight theorem proving and meta-programming. I am struggling to see what global mechanism requires a weird linker step. I also don't understand what you mean when you say that the logical aspect could be a parameter.

Why can't we add a default that prints "<unknown type>" (or, even better "<unknown type X>")? IMO, we should be able to do that;

You're describing the OverlappingInstances extension. And you can "do that" (for some value of "that") quite successfully, with a bit of discipline. (As Keean et al demonstrated with HList in 2004 hooray!)

If you want to be able to say <unknown type X> then you need a constraint that the type be Typeable, so that you can get a text representation of the type. Similarly "How do we get an instance of Show here": put a constraint on the class; or at least on the instance.

You have to impose the disciplines for overlap not just in your instances, but also on anybody who imports them or functions using them. So OverlappingInstances is notoriously brittle in face of separate compilation. (The 'orphan instances' problem.)

Perhaps it could be improved with backtracking/global instance search, as Keean suggests (and there's proposals/prototypes out there). But there is every possibility of small/apparently unrelated changes to the code triggering a different selection; also of backtracking never terminating. So GHC HQ has always resisted it. And I think that's appropriate for an industrial compiler, as opposed to an experimental language (which Haskell isn't any more).

Subtyping (in the OOP sense) is a whole other kettle of fish. Haskell just doesn't do it, never has never will IMO. I don't miss it.

I think overlapping instances demonstrates the problem. Add the default instance of Show with an overlapping instance and you'll then be able to compile my snippet for foo above. But you'll find that no other instance of Show is ever used by foo, e.g. (foo 'string') evaluates to "< unknown type>". And this is what we want (otherwise we'd violate parametricity). But it seems to conflict with the typecase semantics in use elsewhere.

But you'll find that no other instance of Show is ever used by foo

You have to make foo a method of a class that despatches on its argument's type. (Or make it call such a method -- in which case you need a constraint on foo's type.) And you have to switch on OverlappingInstances, of course.

Instance selection/despatch is typecase semantics. It's the same semantics used by GADTs under the hood -- which is why "qualified types" is another good name for GADTs.

OverlappingInstances does risk violating parametricity -- which is why I said "brittle". You need whole-of-program logic that gathers together all instances for a class, and validates them for consistency, and figures out (in effect) the type-level case for instance selection.

You have to make foo a method of a class that despatches on its argument's type.

Why do you have to do that? What semantics are being followed if you just write foo as I have?

Thanks for the link to the QuantifiedConstraints paper. That's interesting.

What semantics are being followed if you just write foo as I have?

If you write bare foo = show, the inferred type you get is foo :: forall a. (Show a) => a -> String. IOW you get a constraint on foo's type like it or not.

If you try to give a signature foo :: forall (a :: *). a -> String with that definition, you'll get ERROR - Cannot justify constraints in explicitly typed binding or similar.

So if you "just write foo as I have", you get no semantics. You haven't provided a type-level means to despatch on the argument's type. Therefore the only expressions you can write must be parametric polymorphic in the argument. That's just how overloading works. (That's not specific to Haskell.)

You could easily try all this for yourself, by the way. There's plenty of places to try Haskell online, if you don't want to install it. Then you'll be able to give syntactically correct examples.

class Foo a where
    foo :: a -> String

instance Foo a where
    foo x = "Did not find overlap"

instance Foo [a] where
    foo x = "Found overlap"

bar :: a -> String
bar x = foo [x]

baz :: a -> String
baz x = foo x

main = do
    print $ bar 1
    print $ baz [1]

Output:

"Found overlap"
"Did not find overlap"

Probably will continue to write code without checking it. Sorry.

You've given a signature for baz, which has had the effect of removing the instance constraint/making it more general.

Take the signature out; you'll get "Found overlap" in both expressions. Then you don't need IncoherentInstances.

I said you need "discipline" to use OverlappingInstances. If you've switched on IncoherentInstances, you've abandoned discipline -- as the name should tell you. Don't do that. If GHC tells you it can't resolve instances (as it does in this case), then fix the signatures.

I still don't like typecase semantics.

On overlapping instances, I am tending to favour not allowing them, and instead allowing type disequality. This has much nicer properties than negation, you can just defer solving until the type variable is grounded or propagate the disequality constraint. You can achieve the same results as overlapping instances but with stability.

Disequality also makes you realise how special equality is, because you can solve equality by unification of type variables, but this is really a special case of constraint propagation. It also makes the open/closed distinction obvious because A != 2 is a finite set when closed and an infinite set when open. What's interesting is if we just propagate the constraint as a constraint on unification we don't need to know if it's open or closed.

allowing type disequality. This has much nicer properties than negation, ...

To bring this discussion full circle. There's a proposal for that, too. (Please upvote and/or comment there.)

Disequality works even better with instance selection, because without functional dependencies instance resolution is in the 'in' mode (as in Prolog argument modes), which means we have to already have a ground type, so with Haskell there would be no need to defer solving.

On the other hand you miss out on some things without allowing overlapping, and I like the idea of being able to abstract at the type class level, which seems to require overlapping and backtracking, allowing definition of constraints like "memberOf". I think controlling scope is the solution here. Disequality would in general be preferred, but you would allow overlapping locally within a module.

Perhaps an 'other' default instance could remove some of the remaining need for overlapping, it would be anti-modular in the sense that behaviour could be modified by adding new instances, but it seems less problematic.

However for optimisation and proof search you seem to need overlapping, as there are different paths to try.

... it would be anti-modular ...

Sorry Keean, but that's the road to madness. The only people who want local/scoped instances are those who haven't thought hard enough about overall program coherence. Probe their proposals with some even quite simple multi-module examples, and it turns to dust. You lose parametricity, as Matt pointed out.

It depends on what you want instances for. Certainly for a global property like "Showable" you don't want it.

However if you want to proof search you need overlapping instances and backtracking. For example if you want to prove A is convertible to B you will need to search all the paths to find a valid sequence of transforms.

Overlapping instances would be problematic globally because other modules could change the behaviour. By restricting them to the local module you can get coherence because you cannot change the behaviour from outside.

Where's the problem?

Edit: I've just realised I have been imprecise with my terminology, I meant local type-classes not local instances. So overlapping would only be allowed where all the instances are defined in the same module, effectively a closed typeclass.

I haven't done a good job of expressing my concerns with GADTs or type classes or type families. ...
The problem to me is that we've conflated the static descriptor of types, which we should be able to inspect and use for meta-programming, with the logical proposition or set denoted by the type.

I'm not atall getting your concern here. Haskell has a nominative type system: a type has a name. Your meta-programming needs only to look at the name. (Also with recent extensions for PolyKinds and type-in-type, a type belongs to a type-of-type, formerly known as Kind -- which has a name.)

Classes, instances, GADTs, Type Families despatch by type name. Inside classes/instances, the methods certainly treat types as sets of values. But that's not meta-programming.

And beware that a) a type might denote an empty set of values; but b) every type is inhabited by bottom; compounded by c) you cannot test whether bottom is the only inhabitant.

Meta-programming in Haskell is not logic programming. The compiler 'infers' in only ways to do with type refinement/solving. Implementing it for theorem-proving would make compilation undecidable/non-terminating in general.

And yet ... look at the recent proposal (and prototype/limited implementation) for QuantifiedConstraints the expressive power of first-order logic, according to the hs2017 paper. That paper's logic/prototype does include backtracking; but the GHC limited implementation doesn't.

And Keean is right that nothing takes advantage of data types (not just GADTs) being closed -- not even with DataKinds. That's a frequent trap for newbies.