Re: [Haskell-cafe] 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.