Re: equality relations: user-facing pretty-printing question

Ryan Scott

18 Jan 2016 18 Jan '16

5:24 p.m.

In my ideal world, GHC would remember as much as what the user wrote as possible in printing error messages. So if the user writes: f :: Int ~ Char => ... Then GHC would remember that the context was written with a single tilde, and print out Int ~ Char in the error message explicitly wherever the full type signature of f is printed. What it sounds like, though, is that deep in the guts of the type inferencer, there's a chance that single-tilde equality might turn into double-tilde or tilde-hash equality at some point. In those cases, printing out the particular brand of tilde might get confusing. In such cases, we might compromise and print out something neutral like "is equal to". I suppose this would always be the case if you didn't explicitly write a ~ b and had to infer it. I'm not sure about the technical details of this though, i.e., if GHC actually remembers a ~ b all the way through the typechecking/inferencing pipeline. Ryan S.

Show replies by date

Iavor Diatchki

18 Jan 18 Jan

5:52 p.m.

New subject: equality relations: user-facing pretty-printing question

Hello, What's the difference between `~~` and `~#` (I assume `~#` is heterogeneous)? As for the rest, as far as I understand, `~` is a strict subset of `~~` in the sense that: 1. if `a ~ b`, then `a ~~ b` 2. if `not (a ~ b)`, then `not (a ~~ b)` 3. if `a ~ b` is a kind error (i.e., the kind of `a` is known to be different from the kind of `b`), then `not (a ~~ b)` So, perhaps it makes sense to have a "smart" pretty printer for `a ~ b`: if kindOf a == kindOf b then `a ~ b` else `a ~~ b` -Iavor On Mon, Jan 18, 2016 at 9:24 AM, Ryan Scott wrote:

...

In my ideal world, GHC would remember as much as what the user wrote as possible in printing error messages. So if the user writes:

f :: Int ~ Char => ...

Then GHC would remember that the context was written with a single tilde, and print out Int ~ Char in the error message explicitly wherever the full type signature of f is printed.

What it sounds like, though, is that deep in the guts of the type inferencer, there's a chance that single-tilde equality might turn into double-tilde or tilde-hash equality at some point. In those cases, printing out the particular brand of tilde might get confusing. In such cases, we might compromise and print out something neutral like "is equal to". I suppose this would always be the case if you didn't explicitly write a ~ b and had to infer it.

I'm not sure about the technical details of this though, i.e., if GHC actually remembers a ~ b all the way through the typechecking/inferencing pipeline.

Ryan S. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Richard Eisenberg

5:55 p.m.

New subject: equality relations: user-facing pretty-printing question

I like that idea. Do others? Yes, agreed about the difference between ~ and ~~. ~# is unlifted, and is now the type that the solver works on. ~~ is lifted. That's the only difference. But the fact that ~~ is lifted is what allows you to put it in a constraint, because all constraints are lifted. Users should never bother with ~#, but they might with ~~. Richard On Jan 18, 2016, at 12:52 PM, Iavor Diatchki wrote:

...

Hello,

What's the difference between `~~` and `~#` (I assume `~#` is heterogeneous)?

As for the rest, as far as I understand, `~` is a strict subset of `~~` in the sense that: 1. if `a ~ b`, then `a ~~ b` 2. if `not (a ~ b)`, then `not (a ~~ b)` 3. if `a ~ b` is a kind error (i.e., the kind of `a` is known to be different from the kind of `b`), then `not (a ~~ b)`

So, perhaps it makes sense to have a "smart" pretty printer for `a ~ b`:

if kindOf a == kindOf b then `a ~ b` else `a ~~ b`

-Iavor

On Mon, Jan 18, 2016 at 9:24 AM, Ryan Scott wrote: In my ideal world, GHC would remember as much as what the user wrote as possible in printing error messages. So if the user writes:

f :: Int ~ Char => ...

Then GHC would remember that the context was written with a single tilde, and print out Int ~ Char in the error message explicitly wherever the full type signature of f is printed.

What it sounds like, though, is that deep in the guts of the type inferencer, there's a chance that single-tilde equality might turn into double-tilde or tilde-hash equality at some point. In those cases, printing out the particular brand of tilde might get confusing. In such cases, we might compromise and print out something neutral like "is equal to". I suppose this would always be the case if you didn't explicitly write a ~ b and had to infer it.

I'm not sure about the technical details of this though, i.e., if GHC actually remembers a ~ b all the way through the typechecking/inferencing pipeline.

Ryan S. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

David Kraeutmann

6:02 p.m.

New subject: equality relations: user-facing pretty-printing question

If ~# is hidden from the user, I think it's reasonable to hide it as an implementation detail. The idea Iavor had sounds good, but we can get (potentially) confusing error messages when writing `Int ~~ Char => ...` -- the smart pretty printer would print `Int ~ Char`. Might get a bit messy. On 1/18/2016 6:55 PM, Richard Eisenberg wrote:

...

I like that idea. Do others?

Yes, agreed about the difference between ~ and ~~.

~# is unlifted, and is now the type that the solver works on. ~~ is lifted. That's the only difference. But the fact that ~~ is lifted is what allows you to put it in a constraint, because all constraints are lifted. Users should never bother with ~#, but they might with ~~.

Richard

On Jan 18, 2016, at 12:52 PM, Iavor Diatchki wrote:

...
Hello,

What's the difference between `~~` and `~#` (I assume `~#` is heterogeneous)?

As for the rest, as far as I understand, `~` is a strict subset of `~~` in the sense that: 1. if `a ~ b`, then `a ~~ b` 2. if `not (a ~ b)`, then `not (a ~~ b)` 3. if `a ~ b` is a kind error (i.e., the kind of `a` is known to be different from the kind of `b`), then `not (a ~~ b)`

So, perhaps it makes sense to have a "smart" pretty printer for `a ~ b`:

if kindOf a == kindOf b then `a ~ b` else `a ~~ b`

-Iavor

On Mon, Jan 18, 2016 at 9:24 AM, Ryan Scott wrote: In my ideal world, GHC would remember as much as what the user wrote as possible in printing error messages. So if the user writes:

f :: Int ~ Char => ...

Then GHC would remember that the context was written with a single tilde, and print out Int ~ Char in the error message explicitly wherever the full type signature of f is printed.

What it sounds like, though, is that deep in the guts of the type inferencer, there's a chance that single-tilde equality might turn into double-tilde or tilde-hash equality at some point. In those cases, printing out the particular brand of tilde might get confusing. In such cases, we might compromise and print out something neutral like "is equal to". I suppose this would always be the case if you didn't explicitly write a ~ b and had to infer it.

I'm not sure about the technical details of this though, i.e., if GHC actually remembers a ~ b all the way through the typechecking/inferencing pipeline.

Ryan S. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Ryan Scott

6:02 p.m.

New subject: equality relations: user-facing pretty-printing question

That sounds like a great idea to me. Ryan S.

Eric Seidel

6:12 p.m.

New subject: kind of type equalities (was: equality relations: user-facing pretty-printing question)

This is a bit tangential, but I find it odd that we care about whether a type equality has kind Lifted or Unlifted. As I understand, the Lifted/Unlifted distinction exists so that we know whether we have a thunk (and by extension a pointer of a constant size) or the thing itself (the size depends on the type). So Lifted/Unlifted is primarily important for code-gen and runtime purposes. Type equalities, on the other hand, shouldn't exist at runtime as the types are erased. So why do we care whether a type equality is a thunk? My guess is that we only care because type equalities *do* exist in Core as proof terms, so they need to be well-kinded, but this isn't a very satisfying answer. On Mon, Jan 18, 2016, at 09:55, Richard Eisenberg wrote:

...

I like that idea. Do others?

Yes, agreed about the difference between ~ and ~~.

~# is unlifted, and is now the type that the solver works on. ~~ is lifted. That's the only difference. But the fact that ~~ is lifted is what allows you to put it in a constraint, because all constraints are lifted. Users should never bother with ~#, but they might with ~~.

Richard

On Jan 18, 2016, at 12:52 PM, Iavor Diatchki wrote:

...
Hello,

What's the difference between `~~` and `~#` (I assume `~#` is heterogeneous)?

As for the rest, as far as I understand, `~` is a strict subset of `~~` in the sense that: 1. if `a ~ b`, then `a ~~ b` 2. if `not (a ~ b)`, then `not (a ~~ b)` 3. if `a ~ b` is a kind error (i.e., the kind of `a` is known to be different from the kind of `b`), then `not (a ~~ b)`

So, perhaps it makes sense to have a "smart" pretty printer for `a ~ b`:

if kindOf a == kindOf b then `a ~ b` else `a ~~ b`

-Iavor

On Mon, Jan 18, 2016 at 9:24 AM, Ryan Scott wrote: In my ideal world, GHC would remember as much as what the user wrote as possible in printing error messages. So if the user writes:

f :: Int ~ Char => ...

Then GHC would remember that the context was written with a single tilde, and print out Int ~ Char in the error message explicitly wherever the full type signature of f is printed.

What it sounds like, though, is that deep in the guts of the type inferencer, there's a chance that single-tilde equality might turn into double-tilde or tilde-hash equality at some point. In those cases, printing out the particular brand of tilde might get confusing. In such cases, we might compromise and print out something neutral like "is equal to". I suppose this would always be the case if you didn't explicitly write a ~ b and had to infer it.

I'm not sure about the technical details of this though, i.e., if GHC actually remembers a ~ b all the way through the typechecking/inferencing pipeline.

Ryan S. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Richard Eisenberg

6:26 p.m.

New subject: kind of type equalities (was: equality relations: user-facing pretty-printing question)

And lifted ones can exist at runtime, via deferred type errors. With deferred type errors, a lifted equality might be a thunk that evaluates to a type error. I also think that "because Core needs it" is a satisfying answer. That's why we have coercions. If we didn't care about type-checking Core, we could just omit very large swathes of GHC. But then we'd have a non-working compiler. :) Richard On Jan 18, 2016, at 1:12 PM, Eric Seidel wrote:

...

This is a bit tangential, but I find it odd that we care about whether a type equality has kind Lifted or Unlifted.

As I understand, the Lifted/Unlifted distinction exists so that we know whether we have a thunk (and by extension a pointer of a constant size) or the thing itself (the size depends on the type). So Lifted/Unlifted is primarily important for code-gen and runtime purposes. Type equalities, on the other hand, shouldn't exist at runtime as the types are erased.

So why do we care whether a type equality is a thunk? My guess is that we only care because type equalities *do* exist in Core as proof terms, so they need to be well-kinded, but this isn't a very satisfying answer.

On Mon, Jan 18, 2016, at 09:55, Richard Eisenberg wrote:

...
I like that idea. Do others?

Yes, agreed about the difference between ~ and ~~.

~# is unlifted, and is now the type that the solver works on. ~~ is lifted. That's the only difference. But the fact that ~~ is lifted is what allows you to put it in a constraint, because all constraints are lifted. Users should never bother with ~#, but they might with ~~.

Richard

On Jan 18, 2016, at 12:52 PM, Iavor Diatchki wrote:

...
Hello,

What's the difference between `~~` and `~#` (I assume `~#` is heterogeneous)?

As for the rest, as far as I understand, `~` is a strict subset of `~~` in the sense that: 1. if `a ~ b`, then `a ~~ b` 2. if `not (a ~ b)`, then `not (a ~~ b)` 3. if `a ~ b` is a kind error (i.e., the kind of `a` is known to be different from the kind of `b`), then `not (a ~~ b)`

So, perhaps it makes sense to have a "smart" pretty printer for `a ~ b`:

if kindOf a == kindOf b then `a ~ b` else `a ~~ b`

-Iavor

On Mon, Jan 18, 2016 at 9:24 AM, Ryan Scott wrote: In my ideal world, GHC would remember as much as what the user wrote as possible in printing error messages. So if the user writes:

f :: Int ~ Char => ...

Then GHC would remember that the context was written with a single tilde, and print out Int ~ Char in the error message explicitly wherever the full type signature of f is printed.

What it sounds like, though, is that deep in the guts of the type inferencer, there's a chance that single-tilde equality might turn into double-tilde or tilde-hash equality at some point. In those cases, printing out the particular brand of tilde might get confusing. In such cases, we might compromise and print out something neutral like "is equal to". I suppose this would always be the case if you didn't explicitly write a ~ b and had to infer it.

I'm not sure about the technical details of this though, i.e., if GHC actually remembers a ~ b all the way through the typechecking/inferencing pipeline.

Ryan S. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Eric Seidel

6:45 p.m.

New subject: kind of type equalities (was: equality relations: user-facing pretty-printing question)

On Mon, Jan 18, 2016, at 10:26, Richard Eisenberg wrote:

...

And lifted ones can exist at runtime, via deferred type errors. With deferred type errors, a lifted equality might be a thunk that evaluates to a type error.

Ah, fair point.

...

I also think that "because Core needs it" is a satisfying answer. That's why we have coercions. If we didn't care about type-checking Core, we could just omit very large swathes of GHC. But then we'd have a non-working compiler. :)

I should have elaborated on why I find it unsatisfying :) My point was not that type-checking Core is not desirable enough to warrant tracking the kind of a type equality, rather that perhaps there's a simpler way that doesn't include runtime concerns. For example, perhaps type equalities could have their own kind. But it sounds like we can't actually separate equalities from code-gen/runtime.

David Fox

8:16 p.m.

New subject: equality relations: user-facing pretty-printing question

It is better, but you still might write ~~ and see an error message with ~, right? On Mon, Jan 18, 2016 at 9:55 AM, Richard Eisenberg wrote:

...

I like that idea. Do others?

Yes, agreed about the difference between ~ and ~~.

~# is unlifted, and is now the type that the solver works on. ~~ is lifted. That's the only difference. But the fact that ~~ is lifted is what allows you to put it in a constraint, because all constraints are lifted. Users should never bother with ~#, but they might with ~~.

Richard

On Jan 18, 2016, at 12:52 PM, Iavor Diatchki wrote:

Hello,

What's the difference between `~~` and `~#` (I assume `~#` is heterogeneous)?

As for the rest, as far as I understand, `~` is a strict subset of `~~` in the sense that: 1. if `a ~ b`, then `a ~~ b` 2. if `not (a ~ b)`, then `not (a ~~ b)` 3. if `a ~ b` is a kind error (i.e., the kind of `a` is known to be different from the kind of `b`), then `not (a ~~ b)`

So, perhaps it makes sense to have a "smart" pretty printer for `a ~ b`:

if kindOf a == kindOf b then `a ~ b` else `a ~~ b`

-Iavor

On Mon, Jan 18, 2016 at 9:24 AM, Ryan Scott wrote:

...
In my ideal world, GHC would remember as much as what the user wrote as possible in printing error messages. So if the user writes:

f :: Int ~ Char => ...

Then GHC would remember that the context was written with a single tilde, and print out Int ~ Char in the error message explicitly wherever the full type signature of f is printed.

What it sounds like, though, is that deep in the guts of the type inferencer, there's a chance that single-tilde equality might turn into double-tilde or tilde-hash equality at some point. In those cases, printing out the particular brand of tilde might get confusing. In such cases, we might compromise and print out something neutral like "is equal to". I suppose this would always be the case if you didn't explicitly write a ~ b and had to infer it.

I'm not sure about the technical details of this though, i.e., if GHC actually remembers a ~ b all the way through the typechecking/inferencing pipeline.

Ryan S. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

3466

Age (days ago)

3466

Last active (days ago)

List overview

Download

8 comments

6 participants

participants (6)

David Fox
David Kraeutmann
Eric Seidel
Iavor Diatchki
Richard Eisenberg
Ryan Scott