[Haskell-cafe] Re: Syntax question: class (Monad m) => MonadReader r m | m -> r where

[Austin Seipp]

This message is literate haskell.

> {-# LANGUAGE FunctionalDependencies, MultiParamTypeClasses #-}
> {-# LANGUAGE TypeFamilies, EmptyDataDecls, FlexibleContexts #-}

Just to add on for people watching, a fundep pretty much just says that if:

> class Foo a b | a -> b where
>   bar :: a -> b
>   baz :: b -> a

Then if you have an instance:

> data A -- we hold types abstract for simplicity
> data B
> data C
> 
> u = undefined -- convenience
> 
> instance Foo A B where 
>   bar x = u
>   baz y = u

Then there can be no other instance for the class Foo of the form 'A
x' where x /= B, e.g. it would be invalid to then have:

> -- uncommenting this will error:
> -- instance Foo A C where
> --   bar x = u
> --   baz y = u

Why? We have established in the class declaration that 'a' determines 'b'
and in an actual instance of that class (concretely) stated that in
this case, the type A determines the type B and that relation holds
true for any usage of the class (in something like a constraint.)

The only way the typechecker can resolve that /relation/ is if
(roughly speaking I think) the set of types that can be of type 'b'
given an already known type 'a' are constrained in some way.

If you do not have the fundep, then the class will work and so will
instances, but you will get ambiguous type errs when trying to use
functions of the type class.

> class Foo2 a b where
>   foobar :: a -> b
>   foobaz :: b -> a

In the usage of 'foobar,' with no functional dependency, the compiler
cannot determine the type 'b' because in the instances of of 'Foo' we
do not 'bind' types together in any way, so for any instance of 'Foo A
x' an x could work here:

> instance Foo2 Bool Int where
>    foobar x = u
>    foobaz y = u
> instance Foo2 Bool Char where
>    foobar x = u
>    foobaz y = u
> 

This instance will compile, but attempting to use it does not:

$ ghci ...
GHCi, version 6.8.3: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( fundeps-assoc.lhs, interpreted )
Ok, modules loaded: Main.
*Main> :t foobar
foobar :: (Foo2 a b) => a -> b
*Main> let z = foobar True

<interactive>:1:8:
    No instance for (Foo2 Bool b)
      arising from a use of `foobar' at <interactive>:1:8-18
    Possible fix: add an instance declaration for (Foo2 Bool b)
    In the expression: foobar True
    In the definition of `z': z = foobar True
*Main> 


The compiler is not able to determine what to declare the result type
of 'foobar True' as, since there is both an instance of 'Foo2 Bool'
for multiple types!

However, in the original Foo class we do have a fundep, and so we know
that if we give 'bar' a value of type 'A' then we get a 'B' in return
- hence, the fundep is a relation and constrains the possible values
of the type variable 'b' in the declaration, so the compiler can
figure this out.

*Main> let z = bar (u::A)
*Main> :t z
z :: B
*Main> 

Functional dependencies are a little tricky, but they can basically
set up relations between types however you want to (for example, using
a fundep of 'a -> b, b -> a' specifies a 1-to-1 correlation between
the types which instantiate 'a' and 'b'.)

However, there is an alternative which I think is far easier to grok
and can express the same 'set of equations' - associated types. I
think they are nicer mainly because they make the connections between
types in a /functional/ way, not a relational one (despite the name of
functional dependencies.)

For instance, the Foo class above could be rewritten as:

> class (Show a, Show (Boom a), Eq (Boom a)) => Foo3 a where
>   type Boom a :: *
>   barfoo :: a -> Boom a
>   bazfoo :: Boom a -> a

This states that along with method declarations for an instance we
must also specify a type declaration - 'Boom' is an associated type
synonym that takes one type a, and the overall kind of 'Boom a' is *
(that is, it is a 'fully satured' type.) The functional part is seen
in the instance.

> instance Foo3 Bool where
>   type Boom Bool = Int
>   barfoo x = 10
>   bazfoo y = u

So we can see 'Boom' as a function at the type level, indexed by
types.

*Main> let z = barfoo True
*Main> :t z
z :: Boom Bool
*Main> print (z::Int)
10
*Main> 

In this case evaluation is undefined but we can see that the equation
overall results in a type of 'Int' as the typechecker can unify the
types 'Boom Bool' and Int, even though we have to explicitly type it.

For an even better example, I think the type-vector trick is pretty
cute too (uses GADTs): 

http://thoughtpolice.stringsandints.com/code/haskell/misc/type-vectors.hs

This message is getting somewhat long but, I hope that's an adequate
explanation for those who might be hazy or interested. For more on
associated types you should probably look here:

http://haskell.org/haskellwiki/GHC/Indexed_types#An_associated_type_synonym_example

Austin