Dependent Types

[Jon Fairbairn]

"Dominic Steinitz" <dominic.j.steinitz@britishairways.com> wrote:
> I've managed to crack something that always annoyed me when I used to d=
o
> network programming.
[. . .]
> =

> Suppose I want to send an ICMP packet. The first byte is the type and t=
he
> second byte is the code. Furthermore, the code depends on the type. Now=
 you
> know at compile time that you can't use codes for one type with a diffe=
rent
> type. However, in Pascal (which is what I used to use) you only seemed =
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: redirectData 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.u=
k
31 Chalmers Road                                         jf@cl.cam.ac.uk
Cambridge CB1 3SZ            +44 1223 570179 (after 14:00 only, please!)