[Haskell-cafe] emtpy fundep LHS

[Keean Schupke]

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.