[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

Second instalment.

On Sat, 13 Oct 2018 at 4:04 AM, <camarao at dcc.ufmg.br> wrote:

> ...
>        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
>        variables is at the end of this message), and:
>
>         - 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
>       exported):
>
>             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;
but the technique dates back to 2004/the HList paper at least:

> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181015/344eefcc/attachment.html>