Re: [Haskell-cafe] dependent types

12 Apr 2010

      On Sun, Apr 11, 2010 at 5:54 PM, Jason Dagit  wrote:
...
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').
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
You can combine GADTs with a mirror type for views of that data.

{-# LANGUAGE GADTs, EmptyDataDecls #-}
module GADTSmart (VehicleView(..), Vehicle, Car, Truck,
                  mkCar, mkTruck, view) where
data Car
data Truck

data Vehicle t where
    VCar   :: Int -> Vehicle Car
    VTruck :: Int -> Vehicle Truck

data VehicleView t where
    VVCar   :: Int -> VehicleView Car
    VVTruck :: Int -> VehicleView Truck

view :: Vehicle t -> VehicleView t
view (VCar wt)   = VVCar wt
view (VTruck wt) = VVTruck wt

mkCar :: Int -> Maybe (Vehicle Car)
mkCar wt | wt < 2000 = Just (VCar wt)
         | otherwise = Nothing

mkTruck :: Int -> Maybe (Vehicle Truck)
mkTruck wt | wt >= 2000 = Just (VTruck wt)
           | otherwise  = Nothing

-- Client code that doesn't have access to the VCar or VTruck
-- constructors.

moveAcrossBridge :: Vehicle Car -> IO ()
moveAcrossBridge c = case view c of
                       VVCar wt -> putStrLn $ "Car ("++show wt++") on bridge"

Now you can type your functions with the Vehicle GADT, but only
introduce values of that type using smart constructors. You could use
the VVCar or VVTruck data constructors to create invalid values, but
they won't work your functions.

Anthony

Re: [Haskell-cafe] dependent types

Anthony Cowley