Constraints as a moveable feast?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Constraints as a moveable feast?

AntC
There's the makings of a cute feature in a very old Haskell Language report. (With thanks to the 'Partial Type Constructors' 2019 paper for ferreting this out.)

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

1990 v1.0 Haskell report. Yes that's a type synonym with a constraint. I'll give their examples, though they don't really demonstrate the potential:

    origin :: Point Integer                                         -- we get Num a => wanted then discharged for free
    origin = (0, 0)                                                       -- although the appearance of zero wants Num a anyway

    scale :: (Num a) => a -> Point a -> Point a     -- seems wrong to give explicit Num a
    scale w (x,y) = (w*x, w*y)                                  -- the above sig would be inferred anyway

The feature disappeared without trace in the next year's Language report.

I'm thinking we should be able to write

    scale :: a -> Point a -> Point a                             -- get Num a for free by:
    scale :: a -> (Num a => (a, a)) -> (Num a => (a, a))           -- expand the synonym -- this sig currently illegal
    scale :: Num a => a -> (a, a) -> (a, a)                  -- float the constraints out to the implicit forall

So this isn't specific to type synonyms: in general allow prefixing constraints to any sub-term in a type; type inference floats them to the front of the signature. You can kinda get the effect today (so I don't think this is entirely whacky), by cunning use of dummies and term-level combinators:

    typePoint :: Num a => (a, a)
    typePoint = undefined

    scale w xy = const (undefined `asTypeOf` xy `asTypeOf` typePoint) (w `asTypeOf` fst xy)
    -- inferred scale :: Num a => a -> (a,a) -> (a,a)

(Putting a dummy undefined on RHS to show there's nothing up my sleeves, because the actual expression would unify to the right type anyway.)

You can get maybe cleaner code with PatternSignatures. But it's all workarounds in terms/expressions. I want to do the Right Thing and get it accepted as a stand-alone signature.

A couple of caveats:
* Haskell 1990 didn't have MultiParam Type Classes;
* nor existential quant.

So if a nested constraint mentions both an existential tyvar with narrow scope and a universally quant'd tyvar, can't float out that constraint, have to reject the sig.

The constraint in `type Num a => Point a = ...` appearing to the left of the introduced type syn, is also reminiscent of DatatypeContexts, so we could similarly float out the constraints from those appearing within a sig(?) And this would be a way to put constraints on newtypes similarly(?) (Can't put constraints on those currently, because there's not really a data constructor to bind the class dictionary to. Haskell 1990 didn't have newtypes.)

Or is there something deeply anti-System FC here?

AntC

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Constraints as a moveable feast?

Richard Eisenberg-5
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".

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. Instead, we should understand Point a to expand to (a, a) only when Num a holds. 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.

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

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

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.

Richard

On Aug 17, 2020, at 6:50 AM, Anthony Clayden <[hidden email]> wrote:

There's the makings of a cute feature in a very old Haskell Language report. (With thanks to the 'Partial Type Constructors' 2019 paper for ferreting this out.)

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

1990 v1.0 Haskell report. Yes that's a type synonym with a constraint. I'll give their examples, though they don't really demonstrate the potential:

    origin :: Point Integer                                         -- we get Num a => wanted then discharged for free
    origin = (0, 0)                                                       -- although the appearance of zero wants Num a anyway

    scale :: (Num a) => a -> Point a -> Point a     -- seems wrong to give explicit Num a
    scale w (x,y) = (w*x, w*y)                                  -- the above sig would be inferred anyway

The feature disappeared without trace in the next year's Language report.

I'm thinking we should be able to write

    scale :: a -> Point a -> Point a                             -- get Num a for free by:
    scale :: a -> (Num a => (a, a)) -> (Num a => (a, a))           -- expand the synonym -- this sig currently illegal
    scale :: Num a => a -> (a, a) -> (a, a)                  -- float the constraints out to the implicit forall

So this isn't specific to type synonyms: in general allow prefixing constraints to any sub-term in a type; type inference floats them to the front of the signature. You can kinda get the effect today (so I don't think this is entirely whacky), by cunning use of dummies and term-level combinators:

    typePoint :: Num a => (a, a)
    typePoint = undefined

    scale w xy = const (undefined `asTypeOf` xy `asTypeOf` typePoint) (w `asTypeOf` fst xy)
    -- inferred scale :: Num a => a -> (a,a) -> (a,a)

(Putting a dummy undefined on RHS to show there's nothing up my sleeves, because the actual expression would unify to the right type anyway.)

You can get maybe cleaner code with PatternSignatures. But it's all workarounds in terms/expressions. I want to do the Right Thing and get it accepted as a stand-alone signature.

A couple of caveats:
* Haskell 1990 didn't have MultiParam Type Classes;
* nor existential quant.

So if a nested constraint mentions both an existential tyvar with narrow scope and a universally quant'd tyvar, can't float out that constraint, have to reject the sig.

The constraint in `type Num a => Point a = ...` appearing to the left of the introduced type syn, is also reminiscent of DatatypeContexts, so we could similarly float out the constraints from those appearing within a sig(?) And this would be a way to put constraints on newtypes similarly(?) (Can't put constraints on those currently, because there's not really a data constructor to bind the class dictionary to. Haskell 1990 didn't have newtypes.)

Or is there something deeply anti-System FC here?

AntC
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Constraints as a moveable feast?

AntC
In reply to this post by AntC
> 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

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Constraints as a moveable feast?

Richard Eisenberg-5


On Sep 2, 2020, at 10:18 PM, Anthony Clayden <[hidden email]> wrote:

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". 
Yes, but what about

> pointX :: Point a -> a
> pointX (x, _) = x

? We don't want that type to expand to (Num a => (a, a)) -> a.

 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"?)

Ah. Now I see a bit more of what you're getting at. But I really don't know what it means to expand without adding parens. Expanding a type synonym is an operation on an abstract syntax tree (AST). We often write ASTs by just writing out concrete syntax, and this sometimes requires adding parens. Even so, we're really just operating with ASTs -- and I don't think your "expand without parens" operation is defined on ASTs. For example:

> data a + b = Inl a | Inr b
> foo :: Point a + Point b

I can't imagine we want to expand this to

> foo :: Num a => (a, a) + Num b => (b, b)

which, under usual rules of precedence, becomes

> foo :: Num a => ((a, a) + Num b) => (b, b)

Note how the + binds tighter than the =>.

Richard

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Constraints as a moveable feast?

AntC
In reply to this post by AntC
> 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

Ah. Now I see a bit more of what you're getting at. We want as if the type synonym were an associated type family with a most-general instance

    class Num a => CPoint a  where
      type Point a
    instance Num a => CPoint a  where
      type Point a = (a, a)

The semantics to be as the PTC paper, such that expanding `Point a` always requires a `CPoint a` instance, which will in turn want a `Num a`.
And the expansion to be immediate (as with type synonyms) so that the client can put `Point a` in instance heads, for example.

> But I really don't know what it means to expand without adding parens. ... what about
>    pointX :: Point a -> a
> ... We don't want that type to expand to (Num a => (a, a)) -> a

Ok, it was your using fancy type operators that put me off. We can represent the AST (and show the need for parens) by reverting to prefix syntax, within H98:

    pointX :: (->) (Point a) a     -- needs parens around (Point a)

And yes my naieve syntactic expansion would give the type you show, wot we do not want.

AntC

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Constraints as a moveable feast?

AntC
In reply to this post by AntC


On Thu, Sep 3, 2020 at 2:18 PM Anthony Clayden <[hidden email]> wrote:
> 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".

Heh heh as a wee sidenote to the idea of type synonyms/datatypes making their contexts available, as you put it

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

The 1991 Haskell report that dropped type synonym contexts and specified datatype contexts as we now know them, left something under-specified. SPJ/GHC interpreted it one way, Mark P. Jones/Hugs interpreted differently. It didn't come to light until the H98 report:
http://code.haskell.org/~dons/haskell-1990-2000/msg04066.html
"Phil (Wadler), Mark (P. Jones), Jeff (Lewis)" (and Erik Meijer later in the thread) preferred Hugs's approach, so that went into the standard and into GHC. Phil said "`redundant pollution' is exactly the effect I want to achieve!".

AntC

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.