[Haskell-cafe] dependent types

[Ben Millwood]

On Sun, Apr 11, 2010 at 10:54 PM, Jason Dagit <dagit at codersbase.com> wrote:
> 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

A minor point of syntax: GADT constructors should begin with a capital letter.
A more important point: GADT constructors are useful for some things
but aren't appropriate for this case because they aren't "smart" -
they can't take an Int parameter and then make either a Car or a Truck
depending on its value. A smart constructor will need to account for
the possibility that the parameter isn't valid:

mkCar :: Integer -> Maybe Vehicle
mkCar weight
 | weight > carWeight = Nothing
 | otherwise = Car { weight = weight }
-- or
mkVehicle :: Integer -> Vehicle
mkVehicle weight
 | weight > carWeight = Truck weight
 | otherwise = Car weight

Even with GADTs, you can't pattern match on the constructors unless
you export them, in which case you have to allow for the possibility
that someone might construct an invalid value of the type, so you
might then also need "smart" field labels that retrieve values from
the Vehicle without allowing you to set them as well (as you would be
able to if you exported the field label itself).

Personally I think this approach is all rather OO. The way that seems
most natural to me is:

moveVehicleAcrossBridge :: Bridge -> Vehicle -> Maybe Move
moveVehicleAcrossBridge bridge { maxWeight = max } vehicle { weight = w }
 | w > max = Nothing
 | otherwise = {- ... moving stuff ... -}

so you just test the properties directly as and when they are
interesting to you.