[Haskell-cafe] type families, fun deps, lattices imposed on/by types

[Manuel M T Chakravarty]

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).