[Haskell-cafe] Constraints as a moveable feast?
rae at richarde.dev
Tue Sep 1 21:18:40 UTC 2020
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.
> 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?
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe