[Haskell-cafe] Type-level programming problem

[oleg at pobox.com]

Thomas Schilling wrote:
> data T
> class Foo ns a b c | ns -> a, ns -> b, ns -> c where
>      mkFoo :: ns
>      defaultA :: a
>      defaultB :: c -> IO b
>      defaultC :: [T] -> c
>      f :: c -> b -> a -> (b, Int)

> data DefaultA
> instance Foo ns a b c => Apply DefaultA ns a where
>      apply _ _ = defaultA
>
> but I get:
>
>      Could not deduce (Foo ns1 a b1 c1)
>        from the context (Apply MakeAs ns a, Foo ns a b c)
>        arising from use of `defaultA'

Indeed. Let us examine the inferred type of defaultA:
	*Main> :t defaultA
	defaultA :: (Foo ns a b c) => a

We see it is a value polymorphic over four type variables: ns, a, b,
and c. The type variable 'a' is also the type of the value, so we have
a way to instantiate it. There is no direct way to instantiate the
remaining three. If there were a functional dependency a -> ns, a->b,
a->c, we could have instantiated the remaining variables. But there
are no such dependencies. So, there is really no way we can
ever instantiate the type variables ns, b and c -- and so the typechecker
will complain.

So, we need either a functional dependency a -> ns in the definition
of Foo, or defaultA should have a signature defaultA :: ns -> a
(and ditto for other defaults). As I understand, the function
'defaultA' can be present in different components, identified by
ns. When we write 'defaultA' however, how can we say that we mean
defaultA of component X rather than of component Y? There isn't any
way to name the desired component...

Incidentally, if we represent components by records
	data XRec = XRec { defaultA :: XA }
then the type of defaultA is Xref -> XA. It is the function from the
type of the `namespace'. This seems to suggest the
signature of defaultA should be ns -> a ...

BTW, there are other ways to add the name of the namespace to the
signature of defaultA. For example:
	newtype TaggedT ns a = TaggedT a
	class Foo ns a b c | ... 
	 defaultA :: TaggedT ns a
or
	class Foo ns a b c | ... 
	 defaultA :: ns a

etc.