There was an interesting exchange between the authors of Haskell compilers
back in 1999 (i.e. when there were multiple compilers)
http://web.archive.org/web/20151001142647/http://code.haskell.org/~dons/haskell-1990-2000/msg04061.html
I was trying to simulate SPJ's point of view, using PatternSynonyms.
>
> {-# LANGUAGE DatatypeContexts, PatternSynonyms #-}
>
> data Ord a => TSPJ a = MkTSPJ a a
>
> pattern PatTSPJ :: (Ord a) => () => a -> a -> TSPJ a -- empty
Provided
> pattern PatTSPJ x y = MkTSPJ x y
>
> unPatTSPJ :: TSPJ a -> (a, a) -- no
constraints
> unPatTSPJ (PatTSPJ x y) = (x, y)
>
`unPatSPJ`'s binding rejected `No instance for (Ord a) arising from a
pattern`. If I don't give a signature, inferred `unPatTSPJ :: Ord b => TSPJ
b -> (b, b)`.
Taking the DatatypeContext off the `data` decl doesn't make a difference.
So Pattern syns seem to be giving exactly the 'stupid theta' behaviour.
The User Guide
https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms
says
-
⟨CProv⟩ are the constraints *made available (provided)* by a successful
pattern match.
But it doesn't mean that. It's more like "⟨CProv⟩ are the constraints made
available *in addition to ⟨CReq⟩* (provided union required) by a successful
pattern match."
Or ... is there some way to simulate the up-to-1999 GHC behaviour? (I
happen to agree with SPJ; Wadler wasn't thinking it through; consider for
example constructor classes over type constructors with constraints:
there's nothing in the instance head for the constraint to attach to. Now
that we have GADTs -- which are appropriate for a different job -- that DT
Contexts perhaps were being (ab-)used for -- I agree more strongly with
SPJ.)
With GADTs I could get a `unGSPJ` that doesn't expose/provide the
constraint, but it does that by packing the constraint/dictionary
(polluting) inside the data constructor. Not what I want. As SPJ says
down-thread
"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."
AntC
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
