[Haskell-cafe] Constraints as a moveable feast?

[Anthony Clayden]

> on *Tue Sep 1 21:18:40 UTC 2020, Richard Eisenberg wrote:*
> I see the core idea as a fairly straightforward generalization of the >
"Partial Type Constructors" work -- except that I wouldn't phrase any of >
this as "floating out".


Thanks Richard, but no: I see this as exploring what was the idea in
that brief example in the 1990 Report. (It's very vague, so we're all
speculating.) The example there is a type synonym, which the PTC work
doesn't consider. And putting the constraint syntactically before the
type (synonym/data/new) name suggests to me it's 'outer'.


GHC actually can express a bit what I mean by "floating out". I didn't
realise that at the time of writing the O.P., so I'll rework the
example. I'm correcting it because as you say:

> In a few places, you've expanded Point a as Num a => (a, a). But Point a
> is *not* the same thing as Num a => (a, a). Indeed, you didn't define it
> that way. ...


The library supplier writes:


    {#- LANGUAGE RankNTypes  #-}

    type Num a => Point a = (a, a)     -- proposed

    mkPoint :: a -> a -> Point a       -- pretend to hide the constructor

    mkPoint x y = (x, y)        -- no using numeric ops/no Num needed


The compiler expands the synonym to mkPoint :: a -> a -> Num a => (a, a).

Note no parens around the expansion, unlike my O.P. That expansion is
not valid H98, but it is valid in GHC with RankNTypes. The docos say
it's a Rank-1 type. GHC infers


    mkPoint :: Num a => a -> a -> (a, a)


And that's why I call it "floating out". Longer example below.

The idea is the library writer could later change the implementation
to a datatype or a newtype, etc; or even add a further constraint.
They all carry  the constraint(s) 'outer'; the client code doesn't
need to know about the change.


> Instead, we should understand Point a to expand to (a, a) only when Num a holds.


That might be a valid use case (especially for constrained
classes/type families); but it's not the use case I have in mind.


> So, the occurrence of Point a causes a Num a constraint to arise.
> These Num a constraints then get put into the type. No floating.


We all think the 1991 DatatypeContexts design is daft because it
raises wanted constraints but doesn't "put" them anywhere, so the
client-module programmer has to add them explicitly in signatures. To
improve that, where/how should the compiler "put into the type"? The
client writes

    scale :: a -> Point a -> Point a

    -- expand the synonyms; then float out and squish duplicates

    -- ===> scale :: a -> Num a => (a, a) -> Num a => (a, a)  -- no parens added

    -- ===> scale :: Num a => a -> (a, a) -> (a, a)

The 'no parens' step (different to my O.P.) is valid GHC with
RankNTypes; the last step is as GHC infers today, with Num a floated
out. (Or if you don't like that phrase: "canonicalises",
"simplifies"?)


> Note that types like `(Num a => a) -> a` and `Num a => a -> a`
> (both very valid today) mean quite different things,


Yes; although the first isn't valid H98/wasn't valid in 1990; and I'm
struggling to think of a use case for it, noting there's no
existential quant inside the parens. (It's not Rank-2, but is it plain
Rank-1 or Rank-1-and-a-half?) Anyhoo that was an error on my part.

> I think by rephrasing this without floating, we avoid the trouble with
> existentials, etc., that you are worried about.


I'm not sure on that, but we'll leave it for another day.

> Personally, I would tack this onto "Partial Type Constructors"
> instead of trying to make this happen independently,
> but the two features would go nicely together.


PTCs introduce a lot of heavy machinery; whereas I'm thinking of this
as just-below-the-surface syntactic sugar that gets expanded before
type inference. OTOH this doesn't on its own support `instance Functor
Point`, treating the type synonym as an unapplied constructor -- which
is what the Hughes 1999 paper is tackling. (I have an idea how that
could go using this same syntactic expansion idea.)


Note BTW, that I didn't add any constraints to the data constructors
-- which is all the 1991 design does (and that not consistently).
Constructing a `Point` doesn't need any Num ops/methods. But the type
is supplying a wanted Num a 'outside', because any expression
operating on a Point likely uses arithmetic. Constraints on data
constructors (as with GADTs) I see as orthogonal: there will be use
cases for one alone, the other alone, or both combined.


AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200903/2835531e/attachment.html>