<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">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".<div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">I think by rephrasing this without floating, we avoid the trouble with existentials, etc., that you are worried about.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">Richard<br class=""><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Aug 17, 2020, at 6:50 AM, Anthony Clayden <<a href="mailto:anthony_clayden@clear.net.nz" class="">anthony_clayden@clear.net.nz</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">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.)<div class=""><br class=""></div><div class=""> type Num a => Point a = (a, a)</div><div class=""><br class=""></div><div class="">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:</div><div class=""><br class=""></div><div class=""> origin :: Point Integer -- we get Num a => wanted then discharged for free<br class=""> origin = (0, 0) -- although the appearance of zero wants Num a anyway<br class=""><br class=""> scale :: (Num a) => a -> Point a -> Point a -- seems wrong to give explicit Num a<br class=""> scale w (x,y) = (w*x, w*y) -- the above sig would be inferred anyway<br class=""></div><div class=""><br class=""></div><div class="">The feature disappeared without trace in the next year's Language report.<br class=""></div><div class=""><br class=""></div><div class="">I'm thinking we should be able to write</div><div class=""><br class=""></div><div class=""> scale :: a -> Point a -> Point a -- get Num a for free by:</div><div class=""> scale :: a -> (Num a => (a, a)) -> (Num a => (a, a)) -- expand the synonym -- this sig currently illegal</div><div class=""> scale :: Num a => a -> (a, a) -> (a, a) -- float the constraints out to the implicit forall</div><div class=""><br class=""></div><div class="">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:</div><div class=""><span style="font-family:Arial,Helvetica,sans-serif" class=""><br class=""></span></div><div class=""><span style="font-family:Arial,Helvetica,sans-serif" class=""> typePoint :: Num a => (a, a)</span><br class=""></div> typePoint = undefined<br class=""><div class=""><br class=""></div><div class=""> scale w xy = const (undefined `asTypeOf` xy `asTypeOf` typePoint) (w `asTypeOf` fst xy)<br class=""></div><div class=""> -- inferred <span style="font-family:Arial,Helvetica,sans-serif" class="">scale :: Num a => a -> (a,a) -> (a,a)</span></div><div class=""><br class=""></div><div class="">(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.)</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">A couple of caveats:</div><div class="">* Haskell 1990 didn't have MultiParam Type Classes;</div><div class="">* nor existential quant.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">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.)</div><div class=""><br class=""></div><div class="">Or is there something deeply anti-System FC here?</div><div class=""><br class=""></div><div class="">AntC</div></div>
_______________________________________________<br class="">Haskell-Cafe mailing list<br class="">To (un)subscribe, modify options or view archives go to:<br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="">Only members subscribed via the mailman list are allowed to post.</div></blockquote></div><br class=""></div></div></body></html>