[Haskell-cafe] emtpy fundep LHS

[Robert Dockins]

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)