[Haskell-cafe] Re: dependent types

[Maciej Piechotka]

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