On Sun, Apr 11, 2010 at 5:54 PM, Jason Dagit <da...@codersbase.com> wrote: > On Sun, Apr 11, 2010 at 1:59 AM, Andrew U. Frank > <fr...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe