[Hugs-users] Datatype contexts considered not so harmful

[Anthony Clayden]

My proof-of-concept for this as of last year was flaky. I think I've now
got it robust:

- all DatatypeContexts apply for all constructors, irrespective of which
type params the constructor mentions;
- If a data constructor+fields appears in a pattern match, no constraints
inferred;
- whether using positional or labelled field syntax;
- using field labels as selectors also doesn't infer constraints (they're
as-if pattern matching);
- numeric literals in patterns do raise a Num/Integral/Fractional
constraint ...
- ... even if nested inside a data constructor. (That's something I broke
back in October.)

It turned out to only need a few lines of code added to the compiler. It
was finding _where_ to position them that needed a huge amount of trial and
error.

Back to the glorious GHC 1999 (and even pre-1991) future! And "Bleah!"
right back to Wadler.

AntC


On Mon, 11 Oct 2021 at 19:40, Anthony Clayden <anthony.d.clayden at gmail.com>
wrote:

>
> There's a discussion in May 1999 pointing out the H98 Report is
> "inexplicit" wrt the semantics of pattern matching on datatypes with a
> context.
>
> http://web.archive.org/web/20151208175102/http://code.haskell.org/~dons/haskell-1990-2000/threads.html#04062,
> '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
> types
> >    -- 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
> https://mail.haskell.org/pipermail/haskell-cafe/2004-March/005995.html
>
> 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
> building.)
>
> 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.
>
> AntC
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/hugs-users/attachments/20220728/4382f1e0/attachment.html>