On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank <frank@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