[Haskell-cafe] Constraints as a moveable feast?

[Anthony Clayden]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200817/fc69d121/attachment.html>