Are fundeps the right model at all?
Marcin 'Qrczak' Kowalczyk
qrczak@knm.org.pl
21 Dec 2000 18:32:59 GMT
Could somebody show an example which requires fundeps and cannot be
expressed using a simpler model explained below - a model that I can
even understand? Is the model self-consistent at all?
Each class is associated with a set of subsets of type variables in
its head. Let's call it the set of keys. The intuitive meaning of a
key is that types corresponding to these variables are sufficient to
determine which instance to choose. They correspond to lhss of some
fundeps.
Plain classes without explicitly written keys correspond to having
a single key consisting of all type variables. Keys influence the
typechecking thus:
- A type is unambiguous if for every class constraint in it there
exists its key such that types in the constraint corresponding to
type variables from the key contain no type variables which are
absent in the type itself.
- All class methods must have unambiguous types, i.e. for each method
there must be a key whose all type variables are present in the
method's type.
- For each key, there must be no pair of instances whose heads
projected to the class parameters from the key overlap.
- For each class constraint of an unambiguous type an each its key
there must be an instance found basing on this key, or the type is
incorrect because of missing instances. Moreover, instances found
basing on all keys must be identical.
- Perhaps something must be said about class contexts and instance
contexts. I'm not sure what yet.
Examples:
class Collection c e | c where
empty :: c
insert :: c -> e -> c
class Monad m => MonadState s m | m where
get :: m s
put :: s -> m ()
newtype State s a = State {runState :: s -> (a,s)}
instance Monad (State s)
instance MonadState s (State s)
test1:: Int -> Int
test1 x = snd (runState get x) -- Not ambiguous.
class IOvsST io st | io, st where
-- Two single-element keys.
ioToST :: io -> st
stToIO :: st -> io
instance IOvsST (IORef a) (STRef s a) where
ioToST = unsafeCoerce#
stToIO = unsafeCoerce#
test2:: IORef a -> IORef a
test2 = ioToST . stToIO -- Not ambiguous.
class Foo a b | a
instance Foo Int [a]
-- This is rejected by Hugs (with fundep a->b) but I would definitely
-- accept it.
--
__("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
\__/
^^ SYGNATURA ZASTĘPCZA
QRCZAK