Dependent Types

[dominic.j.steinitz@britishairways.com]

Robin,

Thanks very much for this. My problem turned out to be tripping over th=
e
monomorphism restriction. When I looked at this it looked like a candid=
ate
for dependent types but as you point out you can solve this just as wel=
l in
Haskell 98. You save a set of brackets with my approach!

Dominic.




Jon Fairbairn <Jon.Fairbairn@cl.cam.ac.uk>@haskell.org on 16/05/2002
16:45:28

Sent by:  haskell-admin@haskell.org


To:   "Dominic Steinitz" <dominic.j.steinitz
cc:   haskell
bcc:
Subject:  Re: Dependent Types


"Dominic Steinitz" <dominic.j.steinitz@britishairways.com> wrote:
> I've managed to crack something that always annoyed me when I used to=
 do
> network programming.
[. . .]
>
> Suppose I want to send an ICMP packet. The first byte is the type and=
 the
> second byte is the code. Furthermore, the code depends on the type. N=
ow
you
> know at compile time that you can't use codes for one type with a
different
> type. However, in Pascal (which is what I used to use) you only seeme=
d to
> be
> able to carry out run time checks.

I'm not sure I understand your problem.  I don't see what's
wrong with the following approach, which is Haskell 98. The
type byte is coded as the type of the packet. Excuse the
perhaps ideosyncratic style ... (in particular, I'm
expecting people to use import qualified with this).


   module ICMP where

   data Type =3D Redirect RedirectData
          | TimeExceeded TimeData

   {- so you get an alternative for each of the packet types -}

   instance Enum Type where
         fromEnum (Redirect _) =3D 5
         fromEnum (TimeExceeded _) =3D 11

   {- we can't derive Enum for ICMP.Type, because it has non-nullary
      constructors. That just makes it a bit more tedious
      One could provide a class "code" with code:: t -> Int
      instead of fromEnum
    -}

   {- now we define individual record types for each of the different
      ICMP types -}

   data RedirectData =3D RedirectData {redirectCode:: RedirectCode,
                         ip_addr:: Int, -- whatever
                         redirectData:: [Int]} -- or whatever

   data RedirectCode =3D RedirNet
               | RedirHost
               | RedirNetToS
               | RedirHostToS
     deriving Enum

   data TimeData =3D TimeData {timeCode:: TimeExceededCode,
                    timeData:: [Int]} -- or whatever

   data TimeExceededCode =3D ExcTTL
                | ExcFragTime
     deriving Enum

   {- Since Haskell 98 doesn't have MPTCs, if we want to
      encode packets as anything other than [Int] we'd have
      to define more classes.  Encode serves as an example. -}

   class Encode t where
      encode:: t -> [Int]

   instance Encode Type where
         encode p@(Redirect d) =3D fromEnum p: encode d
         encode p@(TimeExceeded d) =3D fromEnum p: encode d

   instance Encode RedirectData where
         encode d =3D fromEnum (redirectCode d): ip_addr d: redirectDat=
a d

   instance Encode TimeData where
         encode d =3D fromEnum (timeCode d): 0: timeData d



so one can go

   encode (Redirect (RedirectData RedirNet 0 [0]))

and get [5,0,0,0], but


   encode (TimeExceeded (TimeData RedirNet 0 [0]))

gives an error, as one would hope. What am I missing?


Cheers,

  J=F3n
--
J=F3n Fairbairn                                 Jon.Fairbairn@cl.cam.ac=
.uk
31 Chalmers Road                                         jf@cl.cam.ac.u=
k
Cambridge CB1 3SZ            +44 1223 570179 (after 14:00 only, please!=
)


_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell







      -----------------------------------------------------------------=
--------------------------------

      Save time by using an eTicket and our Self-Service Check-in Kiosk=
s.
      For more information go to http://www.britishairways.com/eservice=
1
=