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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Nicolas Frisby
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). 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 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-5
This is an interesting proposal. When I started reading it, I wondered why anyone would want to avoid the current definition. But you motivate that part well. I would want a larger test of the IsTrue approach to make sure it does what you want before supporting this. But wait: couldn't you write your GHC.TypeLits.Passive today, in a library, with no ill effect? If so, there isn't a strict reason GHC needs to adopt this. (Of course, if the new definition proves useful, then it might make sense to do so in time.)

> On May 21, 2019, at 3:48 AM, Nicolas Frisby <[hidden email]> wrote:
>
> 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.

If something like this ends up in GHC, Data.Type.Bool seems like the right place.

Richard
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Haskell - Libraries mailing list
In reply to this post by Nicolas Frisby

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 <[hidden email]> On Behalf Of Nicolas Frisby
Sent: 21 May 2019 02:48
To: Haskell Libraries <[hidden email]>
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). 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 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-5
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 <[hidden email]> 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 <[hidden email]> On Behalf Of Nicolas Frisby
Sent: 21 May 2019 02:48
To: Haskell Libraries <[hidden email]>
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). 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 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Nicolas Frisby
In reply to this post by Richard Eisenberg-5
Yes, it seems possible that a user space declaration of <= via IsTrue as in my first email could get much of the desired behavior. I plan on trying it with the work code base soon, maybe even today -- it'll probably do better than my current workaround.

If, however, we want the Nat solver to do anything at all with a Given `IsTrue (n <=? m)`, then I think it will need changes. I don't know that machinery well, but it seems very likely it would ignore such Givens.

For example, I would naively expect the Nat solver should discharge a Wanted `IsTrue (n <=? m)` from two Givens `(IsTrue (n <=? x),IsTrue (x <=? m))`.

Simon's exploration of IsTrue/IsEqual might shed more light on what exactly the Nat solver should and should not do with such a Given. If it's in fact nothing at all, then yes, maybe a user space solution fully supplants the proposed Passive.<=. But I currently anticipate that it should do something with such Givens.

Thanks. -Nick

On Tue, May 21, 2019, 00:29 Richard Eisenberg <[hidden email]> wrote:
This is an interesting proposal. When I started reading it, I wondered why anyone would want to avoid the current definition. But you motivate that part well. I would want a larger test of the IsTrue approach to make sure it does what you want before supporting this. But wait: couldn't you write your GHC.TypeLits.Passive today, in a library, with no ill effect? If so, there isn't a strict reason GHC needs to adopt this. (Of course, if the new definition proves useful, then it might make sense to do so in time.)

> On May 21, 2019, at 3:48 AM, Nicolas Frisby <[hidden email]> wrote:
>
> 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.

If something like this ends up in GHC, Data.Type.Bool seems like the right place.

Richard

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-5
You're right that, without special support, the IsTrue approach won't work with any deductions from Givens. But -- short of strapping on an SMT solver -- we're always going to fall short there, so we should analyze a particular on-the-ground use case before taking any drastic action. (It sounds like you agree with this.)

Richard

On May 21, 2019, at 5:52 PM, Nicolas Frisby <[hidden email]> wrote:

Yes, it seems possible that a user space declaration of <= via IsTrue as in my first email could get much of the desired behavior. I plan on trying it with the work code base soon, maybe even today -- it'll probably do better than my current workaround.

If, however, we want the Nat solver to do anything at all with a Given `IsTrue (n <=? m)`, then I think it will need changes. I don't know that machinery well, but it seems very likely it would ignore such Givens.

For example, I would naively expect the Nat solver should discharge a Wanted `IsTrue (n <=? m)` from two Givens `(IsTrue (n <=? x),IsTrue (x <=? m))`.

Simon's exploration of IsTrue/IsEqual might shed more light on what exactly the Nat solver should and should not do with such a Given. If it's in fact nothing at all, then yes, maybe a user space solution fully supplants the proposed Passive.<=. But I currently anticipate that it should do something with such Givens.

Thanks. -Nick

On Tue, May 21, 2019, 00:29 Richard Eisenberg <[hidden email]> wrote:
This is an interesting proposal. When I started reading it, I wondered why anyone would want to avoid the current definition. But you motivate that part well. I would want a larger test of the IsTrue approach to make sure it does what you want before supporting this. But wait: couldn't you write your GHC.TypeLits.Passive today, in a library, with no ill effect? If so, there isn't a strict reason GHC needs to adopt this. (Of course, if the new definition proves useful, then it might make sense to do so in time.)

> On May 21, 2019, at 3:48 AM, Nicolas Frisby <[hidden email]> wrote:
>
> 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.

If something like this ends up in GHC, Data.Type.Bool seems like the right place.

Richard


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Nicolas Frisby
Yep, agreed. Totally practical.

FYI: my code base at work seems quite happy with the IsTrue approach; a very happy simplification! Like so:

```
class IsTrue
  (msg :: ErrorMessage) (b :: Bool) where
  isTrue :: Proxy# msg -> b :~: 'True

instance IsTrue msg 'True where
  isTrue = \_ -> Refl

instance TypeError msg => IsTrue msg 'False
  isTrue = \_ -> error "impossible"

type (<=) n m = IsTrue (Msg n m) (n GHC.TypeLits.<=? m)

type Msg (n :: Nat) (m :: Nat) =
    'ShowType n
  ':<>:
    'Text " is not <= "
  ':<>:
    'ShowType m
```

(An `absurd` for TypeError might be nice?

Via isTrue, I can explicitly convert between the two <= constraints wherever I need to. Which I could use to explicitly manage those hypothetical hypotheticals we were discussing.

Just to spell it out: the SMT solver would indeed supercede TcTypeNats, but TcTypeNats in turn already supercedes the IsTrue-based encoding. So I've already lost some <= deductions. But my work code doesn't use any of them in this middle ground -- they're all simple enough that IsTrue works as-is or complicated enough that TcTypeNats didn't work already (I'm grumpily writing and invoking Trusted Code Base "axia" in those cases -- I'm avoiding plugin dependencies at work for now.)

On Tue, May 21, 2019, 09:14 Richard Eisenberg <[hidden email]> wrote:
You're right that, without special support, the IsTrue approach won't work with any deductions from Givens. But -- short of strapping on an SMT solver -- we're always going to fall short there, so we should analyze a particular on-the-ground use case before taking any drastic action. (It sounds like you agree with this.)

Richard

On May 21, 2019, at 5:52 PM, Nicolas Frisby <[hidden email]> wrote:

Yes, it seems possible that a user space declaration of <= via IsTrue as in my first email could get much of the desired behavior. I plan on trying it with the work code base soon, maybe even today -- it'll probably do better than my current workaround.

If, however, we want the Nat solver to do anything at all with a Given `IsTrue (n <=? m)`, then I think it will need changes. I don't know that machinery well, but it seems very likely it would ignore such Givens.

For example, I would naively expect the Nat solver should discharge a Wanted `IsTrue (n <=? m)` from two Givens `(IsTrue (n <=? x),IsTrue (x <=? m))`.

Simon's exploration of IsTrue/IsEqual might shed more light on what exactly the Nat solver should and should not do with such a Given. If it's in fact nothing at all, then yes, maybe a user space solution fully supplants the proposed Passive.<=. But I currently anticipate that it should do something with such Givens.

Thanks. -Nick

On Tue, May 21, 2019, 00:29 Richard Eisenberg <[hidden email]> wrote:
This is an interesting proposal. When I started reading it, I wondered why anyone would want to avoid the current definition. But you motivate that part well. I would want a larger test of the IsTrue approach to make sure it does what you want before supporting this. But wait: couldn't you write your GHC.TypeLits.Passive today, in a library, with no ill effect? If so, there isn't a strict reason GHC needs to adopt this. (Of course, if the new definition proves useful, then it might make sense to do so in time.)

> On May 21, 2019, at 3:48 AM, Nicolas Frisby <[hidden email]> wrote:
>
> 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.

If something like this ends up in GHC, Data.Type.Bool seems like the right place.

Richard


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Haskell - Libraries mailing list

I’m afraid I’ve lost sync with this conversation. At some point it’d be good to write up conclusions on a wiki page and/or a ticket, so we don’t lose them.  Email threads are hard to parse later.

 

Simon

 

From: Libraries <[hidden email]> On Behalf Of Nicolas Frisby
Sent: 21 May 2019 18:19
To: Richard Eisenberg <[hidden email]>
Cc: Haskell Libraries <[hidden email]>
Subject: Re: request: a Nat ordering constraint that is not an equality constraint

 

Yep, agreed. Totally practical.

 

FYI: my code base at work seems quite happy with the IsTrue approach; a very happy simplification! Like so:

 

```

class IsTrue

  (msg :: ErrorMessage) (b :: Bool) where

  isTrue :: Proxy# msg -> b :~: 'True

 

instance IsTrue msg 'True where

  isTrue = \_ -> Refl

 

instance TypeError msg => IsTrue msg 'False

  isTrue = \_ -> error "impossible"

 

type (<=) n m = IsTrue (Msg n m) (n GHC.TypeLits.<=? m)

 

type Msg (n :: Nat) (m :: Nat) =

    'ShowType n

  ':<>:

    'Text " is not <= "

  ':<>:

    'ShowType m

```

 

(An `absurd` for TypeError might be nice?

 

Via isTrue, I can explicitly convert between the two <= constraints wherever I need to. Which I could use to explicitly manage those hypothetical hypotheticals we were discussing.

 

Just to spell it out: the SMT solver would indeed supercede TcTypeNats, but TcTypeNats in turn already supercedes the IsTrue-based encoding. So I've already lost some <= deductions. But my work code doesn't use any of them in this middle ground -- they're all simple enough that IsTrue works as-is or complicated enough that TcTypeNats didn't work already (I'm grumpily writing and invoking Trusted Code Base "axia" in those cases -- I'm avoiding plugin dependencies at work for now.)

On Tue, May 21, 2019, 09:14 Richard Eisenberg <[hidden email]> wrote:

You're right that, without special support, the IsTrue approach won't work with any deductions from Givens. But -- short of strapping on an SMT solver -- we're always going to fall short there, so we should analyze a particular on-the-ground use case before taking any drastic action. (It sounds like you agree with this.)

 

Richard



On May 21, 2019, at 5:52 PM, Nicolas Frisby <[hidden email]> wrote:

 

Yes, it seems possible that a user space declaration of <= via IsTrue as in my first email could get much of the desired behavior. I plan on trying it with the work code base soon, maybe even today -- it'll probably do better than my current workaround.

 

If, however, we want the Nat solver to do anything at all with a Given `IsTrue (n <=? m)`, then I think it will need changes. I don't know that machinery well, but it seems very likely it would ignore such Givens.

 

For example, I would naively expect the Nat solver should discharge a Wanted `IsTrue (n <=? m)` from two Givens `(IsTrue (n <=? x),IsTrue (x <=? m))`.

 

Simon's exploration of IsTrue/IsEqual might shed more light on what exactly the Nat solver should and should not do with such a Given. If it's in fact nothing at all, then yes, maybe a user space solution fully supplants the proposed Passive.<=. But I currently anticipate that it should do something with such Givens.

 

Thanks. -Nick

 

On Tue, May 21, 2019, 00:29 Richard Eisenberg <[hidden email]> wrote:

This is an interesting proposal. When I started reading it, I wondered why anyone would want to avoid the current definition. But you motivate that part well. I would want a larger test of the IsTrue approach to make sure it does what you want before supporting this. But wait: couldn't you write your GHC.TypeLits.Passive today, in a library, with no ill effect? If so, there isn't a strict reason GHC needs to adopt this. (Of course, if the new definition proves useful, then it might make sense to do so in time.)

> On May 21, 2019, at 3:48 AM, Nicolas Frisby <[hidden email]> wrote:
>
> 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.

If something like this ends up in GHC, Data.Type.Bool seems like the right place.

Richard

 


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries