[Haskell-cafe] dependent types

[Anthony Cowley]

On Sun, Apr 11, 2010 at 5:54 PM, Jason Dagit <dagit at codersbase.com> wrote:
> On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank
> <frank at 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').
>>
> 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