Re: [Haskell-cafe] Impossible types [was [Haskell-prime]: A question about run-time errors when class members are undefined]

Anthony Clayden

14 Oct 2018 14 Oct '18

6:30 a.m.

Transferring from https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html On Sat, 13 Oct 2018 at 4:04 AM, wrote:

...

Consider for example:

class F a b where f:: a → b class X a where x:: a fx = f x

The type of fx, (F a b, X a) ⇒ b, should not be ambiguous: in distinct contexts, fx can have distinct types (if ambiguity, and 'improvement', are as defined below).

[See the -prime message for the "defined below".] I'm just not seeing why you think any Haskell should accept that. What value could inhabit `fx` except bottom? And indeed no Haskell does accept it, not even GHC with all sorts of nasty extensions switched on, including `AllowAmbiguousTypes`. GHC will accept class `F` with a Functional Dependency `b -> a`, but still I can't 'poke' any value into the `x` argument to `f` in the equation for `fx`. Note: agreeing with this view can lead to far-reaching consequences, e.g.

...

support of overloaded record fields [1,Section 7], ...

There are other ways to support overloaded/duplicate record fields, without doing this much violence to the type system. Look at the `HasField` class using Functional Dependencies, in Adam Gundry's work. polymonads [2] etc.

...

Note that's from a Trac ticket asking for 'dysfunctional' Functional Dependencies. There's a long discussion from the type-inference brains trust coming to no discernable conclusion as to whether it's broken type safety. (Catching incoherence in the Core lint typecheck is not a good look.) a) You've not shown any detailed working of how your proposal gives the type improvement required without also descending into incoherence. b) The combination of Functional Dependencies+Overlapping Instances+Undecidable Instances might be able to cover just enough, but not too much of the requirements (which were never made clear). See my worked examples on that ticket -- some of which are really quite scary. See some of Oleg's work on his ftp site with multi-directional FunDeps and overlaps to achieve injectivity. To try to tame the scariness while still supporting enough power, see the suggestion here https://ghc.haskell.org/trac/ghc/ticket/15632

...

Further examples can be discussed

I have yet to see a convincing use case (from the very lengthy discussions) which couldn't be handled already in GHC. I agree the combination of extensions in GHC (including its bogus consistency check/Trac #10675) can give alarming surprises; but they don't quite break type safety. but this example conveys the

...

main idea that ambiguity should be changed; unlike the example of (show . read), no type annotation can avoid ambiguity of polymorphic fx in current Haskell.

Since `fx` is not accepted in current Haskell, whether you can put a type annotation seems beside the point. AntC [1] Optional Type Classes for Haskell, Rodrigo Ribeiro, Carlos Camarão, Lucília Figueiredo, Cristiano Vasconcellos, SBLP'2016 (20th Brazilian Symposium on Programming Languages), Marília, SP, September 19-23, 2016. [2] https://github.com/carlos1camarao/ghc-proposals/blob/d81c1f26298961ac635ce07...

Attachments:

attachment.html (text/html — 5.4 KB)

Show replies by date

Carlos Camarao

23 Oct 23 Oct

7:13 p.m.

New subject: Impossible types [was [Haskell-prime]: A question about run-time errors when class members are undefined]

...

Transferring from https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html

...

...
On Sat, 13 Oct 2018 at 4:04 AM, wrote: Consider for example:

class F a b where f:: a → b class X a where x:: a fx = f x

The type of fx, (F a b, X a) ⇒ b, should not be ambiguous: in distinct contexts, fx can have distinct types (if ambiguity, and 'improvement', are as defined below).

...

[See the -prime message for the "defined below".] I'm just not seeing why you think any Haskell should accept that. What value could inhabit `fx` except bottom?

The type of fx, (F a b, X a) ⇒ b, is a normal, constrained polymorphic type, in the proposal. When fx is used so that b is instantiated, type variable 'a' will become unreachable. Satisfiability will then be tested: if there is a single instance that satisfies the constraints with the unreachable type variables, these variables will be instantiated and the constrains removed ("type improvement"). For example: -----------A.hs------------------- module A (fx) where class F a b where f:: a -> b class X a where x:: a fx = f x ---------------------------------- ----------- M.hs ----------------- module M (inc) where import A (fx) instance F Int (Int->Int) where f = (+) instance X Int where x = 1 inc = fx ---------------------------------- You cannot define and use fx nowadays in Haskell, even if a functional dependency is inserted and ambiguous types are allowed, because no type improvement is used to instantiate unreachable variables, when unreachable type variables exist. Ok?

...

And indeed no Haskell does accept it, not even GHC with all sorts of nasty extensions switched on, including `AllowAmbiguousTypes`. GHC will accept class `F` with a Functional Dependency `b -> a`, but still I can't 'poke' any value into the `x` argument to `f` in the equation for `fx`.

I hope things are clearer now.

...

...
Note: agreeing with this view can lead to far-reaching consequences, e.g. support of overloaded record fields [1,Section 7], ... There are other ways to support overloaded/duplicate record fields, Of course. without doing this much violence to the type system. Look at the `HasField` class using Functional Dependencies, in Adam Gundry's work.

There is no violence to the type system, just simplification and clean-up.

...

...
polymonads [2] etc. Note that's from a Trac ticket asking for 'dysfunctional' Functional Dependencies. There's a long discussion from the type-inference brains trust coming to no discernable conclusion as to whether it's broken type safety. (Catching incoherence in the Core lint typecheck is not a good look.)

a) You've not shown any detailed working of how your proposal gives the type improvement required without also descending into incoherence.

I don't know why you wonder about incoherence being a problem.

...

b) The combination of Functional Dependencies+Overlapping Instances+Undecidable Instances might be able to cover just enough, but not too much of the requirements (which were never made clear). See my worked examples on that ticket -- some of which are really quite scary. See some of Oleg's work on his ftp site with multi-directional FunDeps and overlaps to achieve injectivity. To try to tame the scariness while still supporting enough power, see the suggestion here https://ghc.haskell.org/trac/ghc/ticket/15632

Perhaps you could select one or two examples for discussion.

...

...
Further examples can be discussed

...

I have yet to see a convincing use case (from the very lengthy discussions) which couldn't be handled already in GHC. I agree the combination of extensions in GHC (including its bogus consistency check/Trac #10675) can give alarming surprises; but they don't quite break type safety.

I think any example of use of any MPTC will be able to be handled, although perhaps differently, with the proposal.

...

...
but this example conveys the main idea that ambiguity should be changed; unlike the example of (show . read), no type annotation can avoid ambiguity of polymorphic fx in current Haskell.

...

Since `fx` is not accepted in current Haskell, whether you can put a type annotation seems beside the point.

fx is accepted in the proposal, as well as (show . read). I thought it was a good example because it is small and illustrates that you cannot accept it and avoid changing the ambiguity rule by just inserting a type annotation. Kind regards, Carlos PS: I was away and couldn't see e-mails last week. On Sun, 14 Oct 2018 at 03:31, Anthony Clayden wrote:

...

Transferring from https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html

On Sat, 13 Oct 2018 at 4:04 AM, wrote:

...
Consider for example:

class F a b where f:: a → b class X a where x:: a fx = f x

The type of fx, (F a b, X a) ⇒ b, should not be ambiguous: in distinct contexts, fx can have distinct types (if ambiguity, and 'improvement', are as defined below).

[See the -prime message for the "defined below".]

I'm just not seeing why you think any Haskell should accept that. What value could inhabit `fx` except bottom?

And indeed no Haskell does accept it, not even GHC with all sorts of nasty extensions switched on, including `AllowAmbiguousTypes`.

GHC will accept class `F` with a Functional Dependency `b -> a`, but still I can't 'poke' any value into the `x` argument to `f` in the equation for `fx`.

Note: agreeing with this view can lead to far-reaching consequences, e.g.

...
support of overloaded record fields [1,Section 7], ...

There are other ways to support overloaded/duplicate record fields, without doing this much violence to the type system. Look at the `HasField` class using Functional Dependencies, in Adam Gundry's work.

polymonads [2] etc.

...
Note that's from a Trac ticket asking for 'dysfunctional' Functional Dependencies. There's a long discussion from the type-inference brains trust coming to no discernable conclusion as to whether it's broken type safety. (Catching incoherence in the Core lint typecheck is not a good look.)

a) You've not shown any detailed working of how your proposal gives the type improvement required without also descending into incoherence.

b) The combination of Functional Dependencies+Overlapping Instances+Undecidable Instances might be able to cover just enough, but not too much of the requirements (which were never made clear). See my worked examples on that ticket -- some of which are really quite scary. See some of Oleg's work on his ftp site with multi-directional FunDeps and overlaps to achieve injectivity. To try to tame the scariness while still supporting enough power, see the suggestion here https://ghc.haskell.org/trac/ghc/ticket/15632

...
Further examples can be discussed

I have yet to see a convincing use case (from the very lengthy discussions) which couldn't be handled already in GHC. I agree the combination of extensions in GHC (including its bogus consistency check/Trac #10675) can give alarming surprises; but they don't quite break type safety.

but this example conveys the

...
main idea that ambiguity should be changed; unlike the example of (show . read), no type annotation can avoid ambiguity of polymorphic fx in current Haskell.

Since `fx` is not accepted in current Haskell, whether you can put a type annotation seems beside the point.

AntC

[1] Optional Type Classes for Haskell, Rodrigo Ribeiro, Carlos Camarão, Lucília Figueiredo, Cristiano Vasconcellos, SBLP'2016 (20th Brazilian Symposium on Programming Languages), Marília, SP, September 19-23, 2016.

[2] https://github.com/carlos1camarao/ghc-proposals/blob/d81c1f26298961ac635ce07...

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Anthony Clayden

25 Oct 25 Oct

5:45 a.m.

New subject: Impossible types [was [Haskell-prime]: A question about run-time errors when class members are undefined]

On Wed, 24 Oct 2018 at 8:20 AM, Carlos Camarao wrote:

...

...
Transferring from

https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html

Carlos, the more I dig into your proposal/the more answers you provide, then the more crazy it's getting. I'll stop after explaining why I say that. I'm absolutely sure I don't want this. SPJ hasn't amplified his "interesting work" comment. You've not indicated if your papers have been peer reviewed nor who by. So in the absence of any independent corroboration, my judgment is there is nothing of merit worth pursuing further. GHC's current combo of FunDeps+Overlap+UndecidableInstances has its problems. That's why I'm always willing to look at alternatives. But not this crazy.

...

...
...
On Sat, 13 Oct 2018 at 4:04 AM, wrote: Consider for example:

class F a b where f:: a → b class X a where x:: a fx = f x

The type of fx, (F a b, X a) ⇒ b, should not be ambiguous: in distinct contexts, fx can have distinct types (if ambiguity, and 'improvement', are as defined below).

...
[See the -prime message for the "defined below".] I'm just not seeing why you think any Haskell should accept that. What value could inhabit `fx` except bottom?

The type of fx, (F a b, X a) ⇒ b, is a normal, constrained polymorphic type, in the proposal. When fx is used so that b is instantiated, type variable 'a' will become unreachable.

Wait ... what? Instantiating a type variable changes some other type variable from reachable to unreachable? I'm already struggling to keep up with your definitions, which are different to GHC's definitions. Type improvement (i.e. instantiating type variables) is supposed to be monotonic: how can it a) affect other type variables that weren't even mentioned in the type assignment; b) have an effect on them opposite of improvement? Satisfiability will then be tested: if there is a single instance that

...

satisfies the constraints

You mean: a single instance in scope. So it's not just that you think scoped instances are a Good Thing (I disagree, for reasons of type safety); You require scoped instances so that there's only one instance visible. What's worse, there's no way to declare for class F that var a is reached from b, as a way to make sure there's only one suitable instance. So I think that means for the (show . read) example that I need to hide all of the Prelude instances, except the one I want for piggy in the middle. with the unreachable type variables, these variables will be

...

instantiated and the constrains removed ("type improvement").

For example:

-----------A.hs------------------- module A (fx) where class F a b where f:: a -> b class X a where x:: a

fx = f x ----------------------------------

----------- M.hs ----------------- module M (inc) where import A (fx) instance F Int (Int->Int) where f = (+) instance X Int where x = 1 inc = fx ----------------------------------

You cannot define and use fx nowadays in Haskell, even if a functional dependency is inserted and ambiguous types are allowed, because no type improvement is used to instantiate unreachable variables, when unreachable type variables exist. Ok?

I am very Ok with how Haskell works. Its definition of 'unreachable' relates to FunDeps. You are now trying to explain Haskell using a different definition of 'unreachable'. I think that's bogus. ...

...

I don't know why you wonder about incoherence being a problem.

I don't know why you think anything you've said shows anything about incoherence. You've given an example with only one instance. Then it's not going to be incoherent with itself. (The discussion I elided was about the polymonads example, for which you've given no solution. Are you again going to require there be only one Monad instance in scope? Is that going to be one instance per module, or at a finer grain? A polymonad combines two Monads to return a third; won't that require at least two pairings in scope?) Coherence is a property of the whole program axiomatisation. I.e. all instances for all classes and constraints. ...

...

Perhaps you could select one or two examples for discussion.

No, the onus is on you to show you are providing equivalent expressivity to what's long been stable in Haskell (GHC and Hugs). And then you have to show you're providing something that improves on it/addresses its difficulties. Let's see a detailed working for polymonads. All we have so far is hand-waving. ... ambiguity rule ...

...

Again, you're using a different definition of "ambiguity", as compared with GHC's `AllowAmbiguousTypes` extension. No wonder it's so hard to follow what you're claiming. AntC

2445

Age (days ago)

2456

Last active (days ago)

List overview

Download

2 comments

2 participants

participants (2)

Anthony Clayden
Carlos Camarao