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