[Hugs-users] Datatype contexts considered not so harmful
anthony.d.clayden at gmail.com
Mon Oct 11 06:40:56 UTC 2021
There's a discussion in May 1999 pointing out the H98 Report is
"inexplicit" wrt the semantics of pattern matching on datatypes with a
'Contexts on datatype declarations', starting at SPJ's opener.
The Report has this example, section 4.2.1:
> data Eq a => Set a = NilSet | ConsSet a (Set a) -- with inferred
> -- NilSet :: forall a. Set a
> -- ConsSet :: forall a. Eq a => a -> Set a -> a
(If, per Wadler's response, he thinks "a type will make no sense without the
constraints", what sense is there in having a `NilSet` without constraints?)
Ref the q SPJ poses, it's _not_ the case that a selector function always
gets the constraint inferred. (As of Hugs 2006 and GHC 8.10.)
If a selector function pattern matches on `ConsSet`, `Eq a =>` is indeed
inferred. But if matching on only `NilSet`, or only on a bare var/wildcard
pattern, no constraint. (In practice of course you would be matching on
`ConsSet`, so this point is purely academic.)
Anyhoo, this behaviour doesn't deliver Wadler's objective. And I find it
weird you have to look at the term level to explain the type. Since `data
Eq a => ...` prefixes the type and constructors, I'd expect the behaviour
to apply at _type_ level.
If I bend Hugs to behave same as-was GHC (no constraint inferred if purely
matching), I get the benefit I can declare instances for constructor
classes (including Foldable) over type constructor `Set`. Whereas the
post-May 199 behaviour disallows this: pattern matching in the method decls
wants an `Eq a =>`, but there's no means to pass in a dictionary.
I can't declare a Functor instance, because building the result applies the
data constructors, so does want a dictionary; again there's no means to
pass one in. I can simulate `fmap` via Foldable's `foldMap`, because that
wants a Monoid instance for the builder, and that does see the element type
as well as the constructor. (The builder can squish out resulting
duplicates, so preserving the invariant of `Set`.) Not being able to
declare `Set` an instance of Functor is a Good Thing. Nor of Monad
As SPJ points out later in the 1999 thread
> But when you take a constructor *apart*, the invariant must hold
> by construction: you couldn't have built the thing you are taking
> apart unless invariant held. So enforcing the invariant again is
> redundant; and in addition it pollutes the type of selectors.
(I note GHC's Pattern Synonyms seem to have fallen into the same hephalump
trap of polluting constraints for matching with constraints needed only for
If you're thinking "but hasn't GHC solved all this with GADTs?" I say no:
their sweet spot is where there's different constraints down the structure;
you can't help but hold a different dictionary at each node and 'Provide'
it on pattern matching. Whereas for `Set` it's crucial you have exactly the
same constraint 'all the way down', and all nodes type `Set a`.
I can (just about) see use cases for datatypes that both have global
contexts and GADT constructors.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Hugs-Users