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)