What GADTs aren't useful for

#1

(Transferring the discussion, because not relevant to that thread.)

Consider a datatype for representing a Set (as a binary tree). We’ll want the elements to be in Ord for efficient searching.

{-# LANGUAGE  DatatypeContexts  #-}
data Ord a => OrdTree a = OrdNil | OrdTree (OrdTree a) a (OrdTree a)

Not a GADT because storing the dictionaries in each node is:

  • Very wasteful. It’s the same dict all the way down.
  • Completely unnecessary: once a node is inserted, there’s no need to introduce ‘local constraints’/the structure already expresses the invariant. [**]
  • If some function wants to compare elements, it will bring its own Ord dict with it. (If it merely wants to scan the elements in sequence, just recursive descent l-to-r.)

What’s really really annoying about DataTypeContexts in the H98 standard is if you merely want to export the tree to a list, you still need to bring an Ord dict.

A lesser annoyance is that because the type of OrdNil doesn’t mention type param a, it doesn’t ask for the dict (evidence that Ord a). So your code can create an empty Tree in one place, then get rejected at some remote place because the empty tree didn’t apply the constraint. (BTW that behaviour I want was spec’d in Haskell vintage 1990, got nixed because implementers were scared of constraints over ungrounded type params.)

These days I can declare the datatype with no constraints. Then use PatternSynonyms to require the constraint for build only. And not export the underlying constructors. That’s just clutter.

[**] GADTs could/should support applying constraints at build but not storing them. That’s what PatterSynonym's weird (Ord a) => () => a -> OrdTree a -> OrdTree a could usefully mean. But the () => is taken as union nothing with the build constraints.

So it’s not merely I find GADTs unhelpful (see the earlier thread); they give the wrong behaviour.

2 Likes
#2

I think you’ll find there are constraints built into the constructors under the hood:

data Term a where
    Lit    :: !Int -> Term Int

-- ===> Lit :: a ~ Int => a -> Term a

So the ~ constraint gets exposed on a pattern match on Lit x.

(Vec appears to be a data family these days, BTW.)

1 Like
#3

This seems indeed like a good example of s problem where GADTs don’t seem to be the best solution; and you’ve provided a good alternative solution using pattern synonyms.

(Though I must say I didn’t understand “the constraint must still be satisfied when converting the ordtree to a list” — if we only need Ord on insert, why not have Ord a => on the insert method rather than on the data type (like containers does)).

1 Like
#4

Indeed, the GADT introduces those equality constraints which are explicitly pattern matched on in Core — but they’re unlike type class constraints which introduce a dictionary needed at runtime — these coercions that are matched on are used in casts needed to make the Core program type check. However, casts and coercions alike are erased at compile time, meaning they don’t incur in any runtime cost (unlike type-class dictionaries).

2 Likes
#5

That’s the rule with DatatypeContexts as is/per H98. Any function touching the datatype must include Ord a =>, whether or not it uses methods from Ord.

Because an empty Set or a singleton still should only be allowed over types in Ord [**]. Data.Set doesn’t export its constructors/only provides functions like insert or toAscList – precisely to avoid users breaking into the abstraction. (Admittedly Data.Set's nodes include tracing stuff, to support efficient rebalancing; users shouldn’t be able to mess with them.)

Because Data.Set doesn’t export its constructors, I can’t do the trick with PatternSynonyms – or at least it needs going round the houses calling methods, not mapping direct to the constructors.

And (for example) I can’t build an efficient scan to get elements within some range of values.

[**] If you’re piggy-backing on Data.Set to implement some kinda Maybe empty/singleton/set for not-necessarily-Ord elements, you’re abusing the type.

1 Like
#6

From a dependent-types perspective, DatatypeContexts seems to be trying but not quite succeeding to introduce a dependent type where the data type is parameterised by the choice of dictionary. In fantasy syntax:

OrdTree : forall (a : Type) -> Ord a -> Type
OrdNil : forall (a : Type)(c : Ord a) . OrdTree a c

This is saying that to even talk about the type of trees, you need to pick an element type and an ordering on that type. The nice thing about this is that it no longer relies on canonicity, because if two trees use different orderings, their types are different.

Unfortunately Haskell is a fair way from making this kind of thing convenient.

4 Likes
#7

Hmm? GHC might be “a fair way” from this. There’s another compiler it’s already implemented. Using the H98 syntax.

I’m not seeing it would be useful for different trees to have same element type but different orderings. (Or you could arrange that via a newtype.)

Then ordinary/H98 constraint-dictionary-lookup-from-type is fit for purpose.

1 Like
#8

I think this example is about introducing constraints to datatypes, which is exactly what the original reply says is not the major use case?

For the OrdTree type, I think the usual approach is to annotate functions that operate on OrdTree a with Ord a. Is this not satisfactory because of performance concerns, or ergonomics?

2 Likes
#9

Hi daylily, I’m not sure what you mean by “this example” nor “original reply” – which is which?

Advocates for GADTs claim they completely supersede H98 Datatype constraints. I’m saying for OrdTree, GADTs are not an improvement; OTOH H98 Datatype constraints aren’t right either; I’d prefer more like Datatype constraints as implemented in GHC up to 1999.

Yes that’s the usual approach. I’m unhappy with that not because of performance but because it fails to show on the datatype (:info for example) that anybody using my datatype is expected to make its elements in Ord. Furthermore Haskell doesn’t insist on that at the point of creating an OrdTree. (Achieve that by hiding the constructors and providing functions like ordNil/singleton/insert which carry the constraint. But now I can’t pattern match. Or use PatternSynonyms. Still fails to show anything for the datatype.)

And of course I have in mind more complex examples with tricky constraints – but still the same constraints ‘all the way down’ the recursive structure.

1 Like