Datatype contexts considered not so harmful

--===============5839913283388831989==
Content-Type: multipart/alternative; boundary="00000000000074a3c205ce0e038d"

--00000000000074a3c205ce0e038d
Content-Type: text/plain; charset="UTF-8"

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

--00000000000074a3c205ce0e038d
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><font face=3D"arial, sans-serif"><br></font><div><font fac=
e=3D"arial, sans-serif">There&#39;s a discussion in May 1999 pointing out t=
he H98 Report is &quot;inexplicit&quot; wrt the semantics of pattern matchi=
ng on datatypes with a context.</font></div><div><font face=3D"arial, sans-=
serif"><a href=3D"http://web.archive.org/web/20151208175102/http://code.has=
kell.org/~dons/haskell-1990-2000/threads.html#04062">http://web.archive.org=
/web/20151208175102/http://code.haskell.org/~dons/haskell-1990-2000/threads=
.html#04062</a>, &#39;Contexts on datatype declarations&#39;, starting at S=
PJ&#39;s opener.<br></font></div><div><font face=3D"arial, sans-serif"><br>=
</font></div><div><font face=3D"arial, sans-serif">The Report has this exam=
ple, section 4.2.1:</font></div><div><font face=3D"arial, sans-serif"><br><=
/font></div><div><font face=3D"arial, sans-serif">&gt;=C2=A0 =C2=A0 data Eq=
 a =3D&gt; Set a =3D NilSet | ConsSet a (Set a)=C2=A0 =C2=A0 =C2=A0-- with =
inferred types<br></font></div><div><font face=3D"arial, sans-serif">&gt;=
=C2=A0 =C2=A0 -- NilSet :: forall a. Set a</font></div><div><font face=3D"a=
rial, sans-serif">&gt;=C2=A0 =C2=A0 -- ConsSet :: forall a. Eq a =3D&gt; a =
-&gt; Set a -&gt; a</font></div><div><font face=3D"arial, sans-serif"><br><=
/font></div><div><font face=3D"arial, sans-serif">(If, per Wadler&#39;s res=
ponse, he thinks &quot;a=C2=A0<span style=3D"color:rgb(0,0,0);font-size:1em=
">type will make no sense without the</span></font></div><div><font face=3D=
"arial, sans-serif"><span style=3D"color:rgb(0,0,0);font-size:1em">constrai=
nts</span>&quot;, what sense is there in having a `NilSet` without constrai=
nts?)</font></div><div><font face=3D"arial, sans-serif"><br></font></div><d=
iv><font face=3D"arial, sans-serif">Ref the q SPJ poses, it&#39;s _not_ the=
 case that a selector function always gets the constraint inferred. (As of =
Hugs 2006 and GHC 8.10.)</font></div><div><font face=3D"arial, sans-serif">=
<br></font></div><div><font face=3D"arial, sans-serif">If a selector functi=
on pattern matches on `ConsSet`, `Eq a =3D&gt;` is indeed inferred. But if =
matching on only `NilSet`, or only on a bare var/wildcard pattern, no const=
raint. (In practice of course you would be matching on `ConsSet`, so this p=
oint is purely academic.)</font></div><div><font face=3D"arial, sans-serif"=
><br></font></div><div><font face=3D"arial, sans-serif">Anyhoo, this behavi=
our doesn&#39;t deliver Wadler&#39;s objective. And I find it weird you hav=
e to look at the term level to explain the type. Since `data Eq a =3D&gt; .=
..` prefixes the type and constructors, I&#39;d expect the behaviour to app=
ly at _type_ level.</font></div><div><font face=3D"arial, sans-serif"><br><=
/font></div><div><font face=3D"arial, sans-serif">If I bend Hugs to behave=
=C2=A0same as-was GHC (no constraint inferred if purely matching), I get th=
e benefit I can declare instances for constructor classes (including Foldab=
le) over type constructor `Set`. Whereas the post-May 199 behaviour disallo=
ws this: pattern matching in the method decls wants an `Eq a =3D&gt;`, but =
there&#39;s no means to pass in a dictionary.</font></div><div><font face=
=3D"arial, sans-serif"><br></font></div><div><font face=3D"arial, sans-seri=
f">I can&#39;t declare a Functor instance, because building the result appl=
ies the data constructors, so does want a dictionary; again there&#39;s no =
means to pass one in. I can simulate `fmap` via Foldable&#39;s `foldMap`, b=
ecause 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 result=
ing duplicates, so preserving the invariant of `Set`.) Not being able to de=
clare `Set` an instance of Functor is a Good Thing. Nor of Monad</font></di=
v><div><font face=3D"arial, sans-serif"><a href=3D"https://mail.haskell.org=
/pipermail/haskell-cafe/2004-March/005995.html">https://mail.haskell.org/pi=
permail/haskell-cafe/2004-March/005995.html</a><br></font></div><div><font =
face=3D"arial, sans-serif"><br></font></div><div><font face=3D"arial, sans-=
serif">As SPJ points out later in the 1999 thread</font></div><div><pre sty=
le=3D"color:rgb(0,0,0)"><font face=3D"arial, sans-serif">&gt;        But wh=
en you take a constructor *apart*, the invariant must hold
&gt;        by construction: you couldn&#39;t have built the thing you are =
taking
&gt;        apart unless invariant held.  So enforcing the invariant again =
is
&gt;        redundant; and in addition it pollutes the type of selectors.</=
font></pre></div><div><font face=3D"arial, sans-serif"><br></font></div><di=
v><font face=3D"arial, sans-serif">(I note GHC&#39;s=C2=A0Pattern Synonyms =
seem to have fallen into the same hephalump trap of polluting constraints f=
or matching with constraints needed only for building.)</font></div><div><f=
ont face=3D"arial, sans-serif"><br></font></div><div><font face=3D"arial, s=
ans-serif">If you&#39;re thinking &quot;but hasn&#39;t GHC solved all this =
with GADTs?&quot; I say no: their sweet spot is where there&#39;s different=
 constraints down the structure; you can&#39;t help but hold a different di=
ctionary at each node and &#39;Provide&#39; it on pattern matching. Whereas=
 for `Set` it&#39;s crucial you have exactly the same constraint &#39;all t=
he way down&#39;, and all nodes type `Set a`.</font></div><div><font face=
=3D"arial, sans-serif"><br></font></div><div><font face=3D"arial, sans-seri=
f">I can (just about) see use cases for datatypes=C2=A0that both have globa=
l contexts and GADT constructors.</font></div><div><font face=3D"arial, san=
s-serif"><br></font></div><div><font face=3D"arial, sans-serif">AntC</font>=
</div><div><br></div></div>

--00000000000074a3c205ce0e038d--

--===============5839913283388831989==
Content-Type: text/plain; charset="utf-8"
MIME-Version: 1.0
Content-Transfer-Encoding: base64
Content-Disposition: inline

X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KSHVncy1Vc2Vy
cyBtYWlsaW5nIGxpc3QKSHVncy1Vc2Vyc0BoYXNrZWxsLm9yZwpodHRwOi8vbWFpbC5oYXNrZWxs
Lm9yZy9jZ2ktYmluL21haWxtYW4vbGlzdGluZm8vaHVncy11c2Vycwo=

--===============5839913283388831989==--