On Mon, 2010-04-12 at 12:44 -0400, Anthony Cowley wrote: > 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
http://www.willamette.edu/~fruehr/haskell/evolution.html {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UndecidableInstances #-} data Zero = Zero data Succ a = Succ a class Peano a where fromPeano :: a -> Integer instance Peano Zero where fromPeano _ = 0 instance forall a. Peano a => Peano (Succ a) where fromPeano _ = 1 + fromPeano (undefined :: a) class (Peano a, Peano b) => LT a b instance Peano b => LT Zero (Succ b) instance LT a b => LT a (Succ b) instance LT a b => LT (Succ a) (Succ b) class (Peano a, Peano b) => EQ a b instance EQ Zero Zero instance EQ a b => EQ (Succ a) (Succ b) class (Peano a, Peano b) => GT a b instance LT a b => GT b a class (Peano a, Peano b) => LEQ a b instance EQ a b => LEQ a b instance LEQ a b => LEQ a (Succ b) class (Peano a, Peano b) => GEQ a b instance EQ a b => GEQ a b instance GEQ a b => GEQ (Succ a) b type One = Succ Zero type Two = Succ One type Three = Succ Two type Four = Succ Three type Five = Succ Four data Car = Car data Truck = Truck data Vehicle s v where VCar :: LT size Five => Vehicle size Car VTruck :: GEQ size Five => Vehicle size Truck Regards
signature.asc
Description: This is a digitally signed message part
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe