[Haskell-cafe] Re: dependent types
Maciej Piechotka
uzytkownik2 at gmail.com
Mon Apr 12 13:56:24 EDT 2010
On Mon, 2010-04-12 at 12:44 -0400, Anthony Cowley wrote:
> 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
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 836 bytes
Desc: This is a digitally signed message part
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20100412/4d8594d8/attachment.bin
More information about the Haskell-Cafe
mailing list