Re: [Haskell-cafe] Constraints as a moveable feast?

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 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.