Isto Aho:
Please, consider the example 03 of "Understanding functional
dependencies
via Constraint Handling rules" by Sulzmann, Duck, Peyton-Jones and
Stuckey.
There we are defining a multiplication over different numeric types:
class Mul a b c | a b -> c where
(*) :: a -> b -> c
instance Mul Int Int Int where ...
instance Mul Int Float Float where ...
Ok, we could add
instance Mul Float Int Float where ...
but if we want to make everything work nicely together, Integer,
Complex,
Rational etc, there will be a lot of instances, especially if we
have to give
both "Float Int" and "Int Float" instances.
And now the question on "lattices of types" (didn't know any better
name
to refer to the following):
Is the following possible? Or can something similar achieved with
type families (easily)?
type lattice T a b
-- Each of the following gives a "<"-relation between types,
-- "upper" gives a method, how we get the larger (2nd) from
-- the smaller (1st).
lattice instance T Int Integer where upper = fromIntegral
lattice instance T Int Float where upper = fromIntegral
lattice instance T Integer (Ratio Integer) where upper = ...
lattice instance T (Ratio Integer) Double where ...
lattice instance T Float Double ...
lattice instance T Double (Complex Double) ...
-- e.g. Now the compiler can check that the top type is
-- unique and that there is a path from every type to the top type.
-- If the compiler founds this not to be the case, an error is output.
-- But otherwise there can be types that are not comparable but
-- the common top is quaranteed to exist.
class Mul a b c where
lattice T
(*) :: a -> b -> c
(*) x y = (upper x y x) * (upper x y y)
-- Now there is no need for the instances like.
instance Mul Int Float Float where ...
instance Mul Float (Ratio Integer) Double where ...
In the definition, the upper function only has one argument...
The compiler can generate those instances, because we have given
the "upper"-methods. There is always the top available.
Function
(*) x y = (upper x y x) * (upper x y y)
might could be replaced with
(*) x y = x * y
because of the presence of lattice T and thus, the "upper"-function.
If this were possible, the benefits would be:
- No need to state "Int Float" and "Float Int" instances on cases
where the operands do commute.
- No need to write a large number of instances if you have several
"types on lattice" (e.g. some more or less well defined relation).
- If the relation between types is not clear, we could define another
lattice T2 to our Mul2 class for the other uses.
Continuing the idea: we could override the default instances generated
by the compiler with our own instances when needed.
Ok, so, is it possible to write something like that already? (I just
wouldn't like write a lot of instances...) If not, would it be
possible to extend, say ghc, to work that way or are there too much
inconsistencies in the above presentation?
Using your idea of separating the lattice and conversion from the
definition of multiplication, you can at least save yourself the class
instances:
{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances,
UndecidableInstances #-}
type family Join a b :: *
type instance Join Int Int = Int
type instance Join Float Float = Float
type instance Join Int Float = Float
type instance Join Float Int = Float
class Conv a b where
conv :: a -> b
instance Conv Int Float where
conv = fromIntegral
instance Conv Int Int where
conv = id
instance Conv Float Float where
conv = id
class Mul a b where
mul :: a -> b -> Join a b
instance (Conv a (Join a b), Conv b (Join a b), Num (Join a b))
=> Mul a b where
mul x y = conv x * conv y
You will have to write quite a lot of type instances of Join.
However, the rest of the code is as concise as you seem to want it.
You could even do better with Join by using more sophisticated type-
level data structures; i.e., you could define type-level association
lists and define Join as a type-level lookup function, including rules
for reflexivity and symmetry, on those lists. In other words, instead
of hard-coding the laws of lattices into the compiler, you'd just
programatically define them as part of your type-level program. This
is more flexible, as I am sure there are other applications, where we
don't want a lattice, but some other structure.
See also Andrew Appleyard's recent BSc thesis on how a similar
approach can be used to embed the type structure of a different
programming language in Haskell. In his case, this was the subtyping
relation of C#:
http://www.cse.unsw.edu.au/~pls/thesis/aja-thesis.pdf
Manuel
PS: The use of UndecidableInstances in the above code is a bit
unfortunate, but it is forced on us by the rather complicated instance
context of Mul (even if the above set of family and class instances is
of course perfectly decidable - GHC just can't tell that easily).
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
