request: a Nat ordering constraint that is not an equality constraint

Tue May 21 09:54:04 UTC 2019

I think the idea is, as Nick describes, that an equality constraint approach might make improvement more powerful (i.e. we get more unifications) but has the unfortunate (but necessary) side effect of making variables untouchable. So neither approach is better than the other, and Nick wants to let users choose which one they want.

Directly responding to Simon's example: Yes I agree with what you say here.

Richard

> On May 21, 2019, at 9:43 AM, Simon Peyton Jones via Libraries <libraries at haskell.org> wrote:
> 
> Therefore many uses of `mkFin` et al *require* that I introduce local equality constraints.  And those sadly spoil lots of desired type inference by making outer tyvars untouchable.
> 
>  
> One would need to think carefully here.  For example, just changing (a~b) to (IsEqual a b) doesn’t really make it less of an equality constraint, does it? Yet (IsEqual a b) isn’t an equality constraint, and hence would not make outer type variables untouchable.  Does that threaten predictable type inference, as an (a~b) constraint does?  I’m not sure.
>  
> Perhaps if it was defined as
>                class IsEqual a b
>                instance IsEqual a a
> all would be well.  But NOT if you defined it as
>                class (a~b) => IsEqual2 a b
>                instance IsEqual2 a a
> because of the superclass.
>  
> Interesting. I’d never thought of that.  cc’ing Richard.
>  
> Simon
>  
> From: Libraries <libraries-bounces at haskell.org> On Behalf Of Nicolas Frisby
> Sent: 21 May 2019 02:48
> To: Haskell Libraries <libraries at haskell.org>
> Subject: request: a Nat ordering constraint that is not an equality constraint
>  
> This email proposes an extension and possible change to GHC.TypeLits module in the core `base` library.
> 
>  
> 
> Is there support for this kind of extension/change to GHC.TypeLits? If so, I'll open a GHC GitLab Issue.
> 
>  
> 
> (If not, I would be very appreciate if someone were able to suggest a nice workaround.)
> 
>  
> 
> # The Proposed Extension
> 
>  
> 
> Please add an alternative to <= that is not defined via ~. For example:
> 
>  
> 
> ```
> 
> module GHC.TypeLits.Passive where
> 
>  
> 
> class IsTrue (a :: Bool)
> 
> instance IsTrue 'True
> 
> instance TypeError ... => IsTrue 'False
> 
>  
> 
> type (<=) x y = IsTrue (x <=? y)
> 
> ```
> 
>  
> 
> as opposed to the existing definition:
> 
> 
> ```
> module GHC.TypeLits where
> 
> type (<=) x y = (x <=? y) ~ 'True
> 
> ```
> 
>  
> 
> Its name should be an operator and should be somewhat obvious -- I can't think of one other than <=, so I hedged here by putting in a new module instead.
> 
> 
> There should be a means of *explicitly* converting back and forth between evidence of the two constraints; they are equi-satisfiable but affect type inference in their scope differently.
> 
> # The Optional Change
> 
> I anticipate most users would prefer Passive.<= to today's <=, so the optional library change in this proposal is to redefine <= and relegate its old definition to a new name. Perhaps:
> 
> ```
> 
> module GHC.TypeLits where
> 
> 
> type (<=) x y = IsTrue (x <=? y)
> 
> type (<=!) x y = (x <=? y) ~ 'True
> 
> ```
> 
>  
> 
> # The Motivation
> 
>  
> 
> I'll explain with an example for some concreteness.  
> 
> I wrote an interface for size-indexed vectors for my employer. It involves some code like this:
> 
>  
> 
> ```
> 
> import GHC.TypeLits
> 
>  
> newtype Fin (n :: Nat) = Unsafe_MkFin{forgetFin :: Integer}
> 
> 
> mkFin :: (KnownNat i,i <= n) => proxy  i -> Fin n
> mkFin = Unsafe_MkFin . natVal
> ```
> 
> Constraints like `(i <= n)` show up throughout the library's interface.
> The problem is that <= is an equality constraint.
> 
> Therefore many uses of `mkFin` et al *require* that I introduce local equality constraints.
> 
> And those sadly spoil lots of desired type inference by making outer tyvars untouchable.
> 
>  
> 
> That's the problem: I have to choose between GHC's specialized solving of <= constraints and unspoiled type inference in their scope.
> 
>  
> 
> # Additional Context
> 
>  
> 
> It is important that today's <= be an equality constraint, because it participates in some constraint improvements that introduce equality constraints.  For example (x <= y,y <= x) implies x ~ y (c.f. the scary https://gitlab.haskell.org/ghc/ghc/issues/16586 <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fissues%2F16586&data=02%7C01%7Csimonpj%40microsoft.com%7Cfd400e22fed34cacdc8108d6dd8e8002%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636940001438800796&sdata=M53kCihvu6RqXOutwOT4Ha7MzPHqmYgcfqzCA1%2BSvYE%3D&reserved=0>). Because <= constraints have the potential to "become" an equality constraint, tyvars outside of a <= constraint must be untouchable in its scope from the get go.
> 
> 
> However, neither my library nor any of its uses relies on such constraint improvements enabled by <= constraints.
> 
> In this context, I would much rather that <= could never "become" an equality constraint, so that it need not be an equality constraint, so that it would never render a tyvar untouchable.
> 
> # An Alternative
> 
> 
> As a partial workaround, I could write
> 
> ```
> data Dict i n = (i <= n) => MkDict
> 
> mkFinD :: (KnownNat i) => Dict i n -> proxy i -> Fin n
> mkFinD MkDict = mkFin
> ```
> 
> and then take pains to only introduce the <= constraints in the argument of `mkFinD`. By limiting the scope of the ~ constraints like that, I could prevent them from spoiling the desired type inference. But it's very cumbersome to manage their scopes manually.
> 
> # Work Estimation
> 
>  
> 
> I just thought of the `IsTrue`-based approach while writing this email, so that detail is somewhat half-baked. It has the right *indicative* semantics, but I doubt today's GHC solver would know what to do with a Given `IsTrue (3 <=? 5)` constraint -- so I'm guessing that exact approach at least would require some significant changes in TcTypeNats.
> 
>  
> 
> Thank you for your time. -Nick
> 
> P.S. - Some of the issue tracker links at https://wiki.haskell.org/Library_submissions#The_Libraries <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwiki.haskell.org%2FLibrary_submissions%23The_Libraries&data=02%7C01%7Csimonpj%40microsoft.com%7Cfd400e22fed34cacdc8108d6dd8e8002%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636940001438810751&sdata=0mdfCDTlrytqy%2Fu4htfH4kF%2F9l9NcJnJNcaPHIi0lRk%3D&reserved=0> respond with 404.
> 
> P.P.S. - Is there a standard place to find something like `IsTrue`? More generally: a test for type equality that does not drive unification? Thanks again.
> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20190521/99ce872a/attachment.html>