[Haskell] Re: A puzzle and an annoying feature

[Martin Sulzmann]

Hi,

Andrew's "problem" is not a typing problem. The problem is due
to the way type classes are implemented.

Note that Oleg's "solution" imposes the exact some improvement
conditions as the FD in Andrew's code. However, Oleg manipulates
the instance declaration and the instance body, so that
the dictionary-passing translation won't fail.

Martin


oleg at pobox.com writes:
 > 
 > Andrew Bromage wrote:
 > 
 > > module FD where
 > >
 > > class C from to | from -> to where
 > >      g :: from -> to
 > >      h :: to -> from
 > >
 > > instance C Char Bool where
 > >      g c = c == 'T'
 > >      h b = if b then 'T' else 'F'
 > >
 > > --f :: (C Char a) => Char -> a
 > > f c = g c
 > 
 > Indeed, functional dependencies are the way to close a class that is
 > _visible_ to the typechecker (unlike the export directive that has no
 > such significance, at least to the inference algorithm).
 > 
 > The problem is that we wish to give 'f' a signature, like the one in
 > the commented code, but we cannot use the type variable 'a'. We must
 > use Bool -- which is silly as the typechecker would have figures it
 > out anyway.
 > 
 > > This is a pretty serious problem when you're doing typeclass
 > > metaprogramming.  In this case, the type you're trying to find is
 > > Bool.  In general, it might be a large complex type, generated by
 > > the class C as a typeclass metaprogram, which you don't want to put
 > > in the type signature for maintainability reasons.
 > 
 > Here's the way to solve the problem -- which is actually the problem
 > with the sequencing of FD resolution and other actions. The following
 > are the changes:
 > 
 > 
 > > instance (TypeCast Bool a, TypeCast a Bool) => C Char a where
 > >      g c = typeCast $ c == 'T'
 > >      h b = if (typeCast b) then 'T' else 'F'
 > >
 > > f :: (C Char a) => Char -> a
 > > f c =  g c
 > >
 > > -- snipped verbatim from the HList library
 > > class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
 > > class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
 > > class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
 > > instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
 > > instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
 > > instance TypeCast'' () a a where typeCast'' _ x  = x
 > 
 > The reason for TypeCast existence is to suitably delay the FD
 > resolution. TypeCast has permitted a lot of code that seemed
 > impossible.
 > 
 > _______________________________________________
 > Haskell mailing list
 > Haskell at haskell.org
 > http://www.haskell.org/mailman/listinfo/haskell