[Haskell-cafe] Re: dependent types

[Maciej Piechotka]

On Sun, 2010-04-11 at 10:59 +0200, 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'). 
> how could one model such situations in haskell? i assume there are
> several possibilities...

I'd model upper type as actuall type and dependants as newtypes of it
with hidden constructors. 

module Car
  (
    Car,
    vehicleToCar,
    carToVehicle,
  )
where
import Vehicle

newtype Car = Car {carToVehicle :: Vehicle}

vehicleToCar :: Vehicle -> Maybe Car
vehicleToCar v | someCondition = Just $! Car v
               | otherwise     = Nothing



Then you can request that:

moveSomeRoad :: Either Car Bicycle -> IO ()
moveSomeRoad = ...

Regards

PS.
If it is possible to define a :-: b which would change (recusivly) a
replacing Either x b into x then you can define 'Vehicle' universe.
However I know too less about type functions to say it for sure.

-------------- 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/20100411/b90ce3b1/attachment.bin