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.