
[Discussion moved from Haskell to Haskell-Cafe] Hi, Regarding - "lazy overlap resolution" aka unique instances Well, if there's only instance which is not exported, then you can use functional dependencies. Assume class C a instance ... => C t Internally, use class C a | -> a instance ... => C t Furthermore, there seems to be an issue that has been overlooked so far. - Providing sufficient type annotations Recall Lennart Augustsson writes:
Here is a small puzzle.
-- The following generates a type error: f :: Char -> Char f c = let x = g c in h x
Lennart "magically" inserted a type annotation to resolve the ambiguity.
-- But this definition does not: f :: Char -> Char f c = let x :: Bool x = g c in h x
Clearly, there are a number of ways to resolve the ambiguity. The Chameleon type debugger assists the user in identifying which locations are responsible. Here's the Chameleon type debugger error message generated for the unannotated function f temp.ch:2: ERROR: Inferred type scheme is ambiguous: Type scheme: forall b. C b => Char -> Char Suggestion: Ambiguity can be resolved at these locations b: f :: Char -> Char f c = let x = g c ^ ^ in h x ^ ^ (The ^ correspond to highlightings of the Chameleon type debugger) This may help the user to realize where and which annotations are missing. E.g., each of the following annotations (there are more possibilities) will do the job. f :: Char -> Char f c = let -- x :: Bool (1) x = g c in h x -- h (x::Bool) (2) -- (h::Bool->Char) x (3) Martin

Martin Sulzmann wrote:
[Discussion moved from Haskell to Haskell-Cafe]
Hi,
Regarding
- "lazy overlap resolution" aka unique instances
Well, if there's only instance which is not exported, then you can use functional dependencies.
Assume
class C a instance ... => C t
Internally, use
class C a | -> a instance ... => C t
But using functional dependencies feels like a sledge hammer, and it is also not Haskell 98. -- Lennart

Lennart Augustsson writes:
[...]
But using functional dependencies feels like a sledge hammer, and it is also not Haskell 98.
Well, I'm simply saying that your proposed extension which is not Haskell 98 can be expressed in terms of a known type class extension. I agree that something weaker than FDs would be sufficient here. Martin

Seeing as we are taling about type class extensions, can you see any problems with the following... class X x instance Int instance Float instance x Here we have overlapping instances... (bad), but if we look at the cases there is one which will match 'x' but never any of the others... that is when the overloading is unresolved... like in: show (read y) suppose we replace X with class X x y | x -> y instance Int Int instance Float Float instance x Int What we mean is for 'x' to catch anything that does not match (not Int or Float)... but this is broken because the programs meaning can change when extra instances are added... But considering above, the 'unresolved condition' is included in x, as well as all the overlapping cases... so is it safe to say: class X x y | x -> y instance Int Int instance Float Float instance (_|_) Int Where (_|_) is some symbol that represents "no match is possible" or a failure of the overloading resolution... This _cannot_ overlap with the other instances, and is distinct (the meaning does not change if instances are added)... This could be used to force resolution in unresolvable cases (much like Integrals default to Integer is ambiguous)... Any thoughts? Keean.

Martin Sulzmann wrote:
Well, if there's only instance which is not exported, then you can use functional dependencies.
Assume
class C a instance ... => C t
Internally, use
class C a | -> a instance ... => C t
The cases I was looking at had more than one instance, but thats cool! (I didn't realise " -> a" was valid syntax without a LHS for the arrow. Oleg has written quite a bit about using fundeps to close classes. Surely you can export this as well - any attempt to add another instance will conflict with the fundep (-> a) which effectively says there can only be one instance as all the LHS will overlap (all being the empty set)?
Furthermore, there seems to be an issue that has been overlooked so far.
- Providing sufficient type annotations
Well in the toy example, yes... but quite often this occurs where the type is derived and extreemly complex - the whole point is you don't really want to be type annotating every assignment. Also you may really want polymorphism, you just have only one instance at the moment. (duing development, or in a user extensible library) Keean.

Keean Schupke wrote:
Martin Sulzmann wrote:
Well, if there's only instance which is not exported, then you can use functional dependencies.
Assume
class C a instance ... => C t
Internally, use
class C a | -> a instance ... => C t
The cases I was looking at had more than one instance, but thats cool! (I didn't realise " -> a" was valid syntax without a LHS for the arrow.
I didn't either. That is cool.
Oleg has written quite a bit about using fundeps to close classes. Surely you can export this as well - any attempt to add another instance will conflict with the fundep (-> a) which effectively says there can only be one instance as all the LHS will overlap (all being the empty set)?
Indeed, it seems to me that one could bootstrap arbitrary closed classes from a class with the (-> a) fundep and multiparameter type classes. (code follows). Then, I should be able to prove some properties of the MyNum class (and type-level programs using it) without worrying about users coming along behind and adding instances. Does this work? Is this what you had in mind? module FunkyNats ( MyNum (...) , Zero , Succ , Twice -- don't export Close ) where -- The unit closed class data Close class Closed a | -> a instance Closed Close -- a closed class build from Closed class (Closed c) => MyNum c a -- the class members data Zero data Succ a data Twice a -- requires access to Close to make instances instance MyNum Close Zero instance (MyNum a) => MyNum Close (Succ a) instance (MyNum a) => MyNum Close (Twice a)

Robert Dockins wrote:
Indeed, it seems to me that one could bootstrap arbitrary closed classes from a class with the (-> a) fundep and multiparameter type classes. (code follows). Then, I should be able to prove some properties of the MyNum class (and type-level programs using it) without worrying about users coming along behind and adding instances. Does this work? Is this what you had in mind?
module FunkyNats ( MyNum (...) , Zero , Succ , Twice -- don't export Close ) where
-- The unit closed class data Close class Closed a | -> a instance Closed Close
-- a closed class build from Closed class (Closed c) => MyNum c a
-- the class members class (Closed c) => MyNum c a data Zero data Succ a data Twice a
-- requires access to Close to make instances instance MyNum Close Zero instance (MyNum a) => MyNum Close (Succ a) instance (MyNum a) => MyNum Close (Twice a)
Yes this seems to require access to the 'Close' constructor in order to add an instance to MyNum. Unfortunatley you also would need access to close to use an instance, but because the second parameters are all distinct, you can add the following fundep to the class: class (Closed c) => MyNum c a | a -> c Now, you can call the class without access to the Close constructor: instance (MyNum c n,MyNum c m) => instance Sum n m ... Keean.
participants (4)
-
Keean Schupke
-
Lennart Augustsson
-
Martin Sulzmann
-
Robert Dockins