<div dir="ltr"><div>> on <i style="color:rgb(0,0,0);font-family:"Times New Roman";font-size:medium">Tue Sep 1 21:18:40 UTC 2020, Richard Eisenberg wrote:</i><span style="font-family:Arial,Helvetica,sans-serif"></span></div>> <span style="color:rgb(0,0,0);font-family:monospace,monospace;font-size:1em;white-space:pre-wrap">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".</span><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">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'.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">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:</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">> 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. ...</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">The library supplier writes:</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    {#- LANGUAGE RankNTypes  #-}</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    type Num a => Point a = (a, a)     -- proposed</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    mkPoint :: a -> a -> Point a       -- pretend to hide the constructor</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    mkPoint x y = (x, y)        -- no using numeric ops/no Num needed</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">The compiler expands the synonym to mkPoint :: a -> a -> Num a => (a, a).</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">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</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    mkPoint :: Num a => a -> a -> (a, a)</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">And that's why I call it "floating out". Longer example below.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">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.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">> Instead, we should understand Point a to expand to (a, a) only when Num a holds.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">That might be a valid use case (especially for constrained classes/type families); but it's not the use case I have in mind.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">> 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.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">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</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    -- expand the synonyms; then float out and squish duplicates</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    -- ===> scale :: a -> Num a => (a, a) -> Num a => (a, a)  -- no parens added</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">    -- ===> scale :: Num a => a -> (a, a) -> (a, a)</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">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"?)</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">> Note that types like `(Num a => a) -> a` and `Num a => a -> a`
> (both very valid today) mean quite different things, </pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">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.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">> I think by rephrasing this without floating, we avoid the trouble with
> existentials, etc., that you are worried about.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">I'm not sure on that, but we'll leave it for another day.
<br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">> 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.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">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.)</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">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.</pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><br></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">AntC</pre></div>