[Haskell-cafe] Constraints as a moveable feast?

[Richard Eisenberg]

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 <anthony_clayden at clear.net.nz> 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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200901/d049aa27/attachment.html>