On Sun, 2010-04-11 at 10:59 +0200, 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...
I'd model upper type as actuall type and dependants as newtypes of it with hidden constructors. module Car ( Car, vehicleToCar, carToVehicle, ) where import Vehicle newtype Car = Car {carToVehicle :: Vehicle} vehicleToCar :: Vehicle -> Maybe Car vehicleToCar v | someCondition = Just $! Car v | otherwise = Nothing Then you can request that: moveSomeRoad :: Either Car Bicycle -> IO () moveSomeRoad = ... Regards PS. If it is possible to define a :-: b which would change (recusivly) a replacing Either x b into x then you can define 'Vehicle' universe. However I know too less about type functions to say it for sure.