Context reduction with functional dependencies?

[Thomas Hallgren]

This is a multi-part message in MIME format.
--------------000008010800080402070402
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit

Hi,

I have been doing an experiment where I use type classes to express
static (compile-time) computations in Haskell. With multi-parameter
classes and functional dependencies, instance declarations can be used
to define function by pattern matching (on the type level). I enclose an
example where I define booleans, natural numbers, a
less-than-or-equal-to function and a maximum function.

In some simple examples (one_lte_two and two_lte_one), it works fine,
but in the last example, where I try to compute the maximum of 1 and 2
in Hugs (hugs -98, February 2000), I get the following error message:

     Type checking
     ERROR "FuncDeps4.hs" (line 27): Unresolved top-level overloading
     *** Binding             : max_one_two
     *** Outstanding context : (Lte Z (S Z) b, If b (S (S Z)) (S Z) c)

Here I expected that the functional dependencies would allow b to be
instantiated to T, and hence c to be instantiated to S (S Z), which
would then be the type of max_one_two. Why doesn't this work?

Regards,
Thomas Hallgren


--------------000008010800080402070402
Content-Type: text/plain;
 name="FuncDeps4.hs"
Content-Transfer-Encoding: 7bit
Content-Disposition: inline;
 filename="FuncDeps4.hs"

module FuncDeps4 where

data T
data F

class If b t e r | b t e -> r
instance If T t e t
instance If F t e e

data Z
data S n
type One = S Z
type Two = S One

class Lte a b c | a b -> c where lte :: a -> b -> c
instance Lte Z b T
instance Lte (S n) Z F
instance Lte a b c => Lte (S a) (S b) c

one_lte_two = lte (u::One) (u::Two) -- :: T
two_lte_one = lte (u::Two) (u::One) -- :: F

class Max a b c | a b -> c where max' :: a -> b -> c
instance (Lte a b l,If l b a c) => Max a b c

-- This doesn't work without the type signature:
max_one_two = max' (u::One) (u::Two)   -- :: Two

u=undefined -- Just a convenient abbreviation


--------------000008010800080402070402--