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

[Anthony Clayden]

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

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/d81c1f26298961ac635ce0724bb76164b418866b/expression-ambiguity.rst

[Anthony Clayden]

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

Second instalment.

...
Ambiguity should be a property of an expression, defined as
follows: if a constraint set C on the constrained type C∪D⇒t of
an expression has unreachable variables, then satisfiability is
tested for C (a definition of reachable and unreachable type
- if there is a single unifying substitution of C with the set
of instances in the current context (module), then C can be
removed (overloading is resolved) and C∪D⇒t 'improved' to
D⇒t;
- otherwise there is a type error: ambiguity if there are two
or more unifying substitutions of C with the set of instances
in the current context (module), and unsatisfiability
otherwise.
2. Allow instances to be imported (all instances are assumed to be
import M (instance A τ₁ ⋯ τₙ , 
 )
specifies that the instance of τ₁ ⋯ τₙ for class A is
imported from M, in the module where the import clause
occurs.
In case of no explicit importation, all instances remain
imported, as currently in Haskell (in order that well-typed
programs remain well-typed).

Consider some typical Read instances from the Haskell Prelude

instance Read a => Read [a] where ...
instance Read a => Read (Maybe a) where ...

Suppose I have `show . read` where the 'piggy in the middle' type is
unreachable (by your definition below); but I want it to be taken as
`(Maybe [Int])`.

Then I arrange my imports of instances to make visible only ... what?

`(Maybe a)` ? Then how do I read the `[a]`? The only instance in scope is
`(Maybe a)`.

`(Maybe [Int])` ? Then how do I decompose the structure to call the
overloads for `read` of the list and of the `Int`? Instance `(Maybe a)` is
not in scope, neither is `[a]` nor `Int`.

And what if in the same module/same scope I want `show . read` where 'piggy
in the middle' is `[Maybe Int]` or `(Maybe [Bool])` ? Then instead of
`Read`, I could create a whole swag of specialised classes/methods:
ReadMaybeListInt, ReadListMaybeInt, ReadMaybeListBool, ... ? But those
could just be regular functions with an explicit signature. Putting an
explicit type annotation on each expression seems a whole lot more
convenient than mucking around with specialised classes or scope of
instances.


Before you answer, consider this very common pattern. It's so common
there's a base library operator for it: type-level `==`
https://downloads.haskell.org/~ghc/latest/docs/html/libraries/base-4.12.0.0/src/Data-Type-Equality.html#%3D%3D;

class TypeEq a a' (b :: Bool) | a a' -> b
instance TypeEq a a True
instance (b ~ False) => TypeEq a a' b

Then an example usage

instance (TypeEq e e' b, TypeIf b This That) => instance Elem e (Cons e'

tail) where ...

Rubric: `Elem` is searching for type `e` in some type-level heterogeneous
list; if found (i.e. `TypeEq` returns `True`), the `TypeIf` despatches to
`This`, else to `That`.

It's crucial for `TypeEq` that both instances are in scope in all places.

Ah, but I see the `TypeEq` example does not contain any "unreachable"
tyvars by your definition below. In which case your specification is silent
as to how type improvement is to behave. (But you claim your approach is
instead of FunDeps; then what is to happen with both instances being able
to unify with the type of some expression?)

Then do you want to change the spec? This was the experience with the
github rounds: the spec kept changing; the examples we'd worked through in
earlier rounds then didn't work with the new spec. Therefore the claims
were impossible to verify with any certainty.

(Definition: [Reachable and unreachable type variables in constraints]
Consider a constrainted type C∪D⇒τ. A variable a ∈ tv(C) is reachable
from V = tv(τ) if a ∈ V or if a ∈ tv(π) for some π ∈ C such that there
exists b ∈ tv(π) such that b is reachable from V; otherwise it is
unreachable.
For example, in (F a b, X a) ⇒ b, type variable 'a' is reachable from
{ b }, because 'a' occurs in constraint F a b, and b is reachable.
Similarly, if C = (F a b, G b c, X c), then c is reachable from {a}.)

AntC

[Carlos Camarao]

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

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?

Post by Anthony Clayden
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.

Post by Anthony Clayden

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

e.g. support of

Post by Anthony Clayden

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

There are other ways to support overloaded/duplicate record fields,

Of course.

Post by Anthony Clayden
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.

Post by Anthony Clayden

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

Post by Anthony Clayden
without also descending into incoherence.

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

Post by Anthony Clayden
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.

Post by Anthony Clayden

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.

Post by Anthony Clayden

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.

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

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/d81c1f26298961ac635ce0724bb76164b418866b/expression-ambiguity.rst
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Anthony Clayden]

Post by Anthony Clayden

Post by Anthony Clayden
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.

Post by Anthony Clayden

Post by Anthony Clayden

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

Post by Anthony Clayden

'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

Post by Anthony Clayden
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

Post by Anthony Clayden
instantiated and the constrains removed ("type improvement").
-----------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.

...

Post by Anthony Clayden
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.


...

Post by Anthony Clayden
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