<div><div dir="auto">Transferring from <div><a href="https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html">https://mail.haskell.org/pipermail/haskell-prime/2018-October/004396.html</a></div></div></div><div dir="auto"><br></div><div dir="auto">Second instalment.</div><div><br><div class="gmail_quote"><div dir="ltr">On Sat, 13 Oct 2018 at 4:04 AM, <<a href="mailto:camarao@dcc.ufmg.br">camarao@dcc.ufmg.br</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">...<br>
Ambiguity should be a property of an expression, defined as<br>
follows: if a constraint set C on the constrained type C∪D⇒t of<br>
an expression has unreachable variables, then satisfiability is<br>
tested for C (a definition of reachable and unreachable type<br>
variables is at the end of this message), and:<br>
<br>
- if there is a single unifying substitution of C with the set<br>
of instances in the current context (module), then C can be<br>
removed (overloading is resolved) and C∪D⇒t 'improved' to<br>
D⇒t;<br>
<br>
- otherwise there is a type error: ambiguity if there are two<br>
or more unifying substitutions of C with the set of instances<br>
in the current context (module), and unsatisfiability<br>
otherwise.<br>
<br>
2. Allow instances to be imported (all instances are assumed to be<br>
exported):<br>
<br>
import M (instance A τ₁ ⋯ τₙ , … )<br>
<br>
specifies that the instance of τ₁ ⋯ τₙ for class A is<br>
imported from M, in the module where the import clause<br>
occurs.<br>
<br>
In case of no explicit importation, all instances remain<br>
imported, as currently in Haskell (in order that well-typed<br>
programs remain well-typed).<br>
</blockquote><div dir="auto"><br></div><div dir="auto">Consider some typical Read instances from the Haskell Prelude</div><div dir="auto"><br></div><div dir="auto">> instance Read a => Read [a] where ...</div><div dir="auto">> instance Read a => Read (Maybe a) where ...</div><div dir="auto"><br></div><div dir="auto">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])`.</div><div dir="auto"><br></div><div dir="auto">Then I arrange my imports of instances to make visible only ... what?</div><div dir="auto"><br></div><div dir="auto">`(Maybe a)` ? Then how do I read the `[a]`? The only instance in scope is `(Maybe a)`.</div><div dir="auto"><br></div><div dir="auto">`(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`.</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">Before you answer, consider this very common pattern. It's so common there's a base library operator for it: type-level `==` <div><a href="https://downloads.haskell.org/~ghc/latest/docs/html/libraries/base-4.12.0.0/src/Data-Type-Equality.html#%3D%3D">https://downloads.haskell.org/~ghc/latest/docs/html/libraries/base-4.12.0.0/src/Data-Type-Equality.html#%3D%3D</a>; but the technique dates back to 2004/the HList paper at least:</div><div dir="auto"><br></div><div dir="auto">> class TypeEq a a' (b :: Bool) | a a' -> b</div><div dir="auto">> instance TypeEq a a True</div><div dir="auto">> instance (b ~ False) => TypeEq a a' b</div><div dir="auto"><br></div><div dir="auto">Then an example usage</div><div dir="auto"><br></div><div dir="auto">> instance (TypeEq e e' b, TypeIf b This That) => instance Elem e (Cons e' tail) where ...</div><div dir="auto"><br></div><div dir="auto">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`.</div><div dir="auto"><br></div><div dir="auto">It's crucial for `TypeEq` that both instances are in scope in all places.</div></div><div dir="auto"><br></div><div dir="auto">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?)</div><div dir="auto"><br></div><div dir="auto">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.</div><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto"><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br><br>
(Definition: [Reachable and unreachable type variables in constraints]<br>
Consider a constrainted type C∪D⇒τ. A variable a ∈ tv(C) is reachable<br>
from V = tv(τ) if a ∈ V or if a ∈ tv(π) for some π ∈ C such that there<br>
exists b ∈ tv(π) such that b is reachable from V; otherwise it is<br>
unreachable.<br>
For example, in (F a b, X a) ⇒ b, type variable 'a' is reachable from<br>
{ b }, because 'a' occurs in constraint F a b, and b is reachable.<br>
Similarly, if C = (F a b, G b c, X c), then c is reachable from {a}.)<br>
<br></blockquote><div dir="auto"><br></div><div dir="auto"><br></div><div dir="auto">AntC</div><div dir="auto"><br></div></div></div>