On Sun, Apr 11, 2010 at 4:15 PM, Ozgur Akgun wrote:

On 11 April 2010 22:54, Jason Dagit wrote:

...

...

...

...

class Vehicle a where

...

data Car data Truck

instance Vehicle Car where instance Vehicle Truck where

Now you can have things that take a Car or a Truck or they can take a Vehicle instead.

moveVehicle :: Vehicle v => v -> Simulation ()

unfortunately, now you cannot use pattern matching while defining moveVehicle.

That's true. Although, if you're writing a simulation where Cars and Trucks are objects in that simulation, they are likely to be defined as records as they will probably have many fields. If that's the case, it's unlikely you'd be using pattern matching with them anyway. It's just a small step from there to using typeclass functions to access the parts you care about. Jason

On Mon, Apr 12, 2010 at 4:32 AM, Ben Millwood wrote:

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.

The problem with this is that it doesn't address the question the OP had. The OP's question was how to enforce things at the type level, but this, while being a valid approach, allows heavy vehicles to attempt the bridge crossing. I agree it's a nice way of encoding it, but if type level enforcement is called for then I don't see how it applies. Jason

On Mon, 2010-04-12 at 12:44 -0400, Anthony Cowley wrote:

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

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