[Haskell-cafe] dependent types

[Jason Dagit]

On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank <frank at geoinfo.tuwien.ac.at
> wrote:

> in modeling real application we have often the case that the type of
> some object depends on a value. e.g. small_boat is a vessel with size
> less than a constant. big_boat is a vessel with a larger size. for
> example, many legal classifications are expressed in this form (e.g. car
> vs. truck)
> depending on the type, operations are applicable or not (e.g. road with
> restriction 'no trucks').
> how could one model such situations in haskell? i assume there are
> several possibilities...
>
>
The two main ways I can think of for this use typeclasses or witness types.

The type class way is like this:
class Vehicle a where

data Car
data Truck

instance Vehicle Car where
instance Vehicle Truck where

Now you can have things that take a Car or a Truck or they can take a
Vehicle instead.

moveVehicle :: Vehicle v => v -> Simulation ()

carsOnly :: Car -> ...

If you want to understand this approach better, I think this is how HList
works to some extent.  For example, see their HBool type class.

Or, you could use witness types:

data Vehicle classification = Vehicle { ... }

mkCar :: Vehicle Car
mkTruck :: Vehicle Truck

Then you would export the smart constructors, (mkCar/mkTruck) without
exporting the Vehicle constructor.

moveVehicle :: Vehicle c -> Simulation ()
carsOnly :: Vehicle Car -> ...

In the witness type version you may find that defining Vehicle as a GADT is
even better:

data Vehicle classification where
  mkCar :: ... -> Vehicle Car
  mkTruck :: ... -> Vehicle Truck

This is nice because it's direct and when you pattern match on the
constructor you recover the type of classification.  For example, I believe
this would type check:

foo :: Vehicle c -> c
foo (mkCar ...) = Car
foo (mkTruck ...) = Truck

(Note: I didn't test any of the above, so I could have errors/typos.)

Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100411/1b67c7dc/attachment.html