Re: Dependent Types

[dominic . j . steinitz]

Robin,

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

Dominic.




Jon Fairbairn <[EMAIL PROTECTED]>@haskell.org on 16/05/2002
16:45:28

Sent by:  [EMAIL PROTECTED]


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


"Dominic Steinitz" <[EMAIL PROTECTED]> 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. Now
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 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 = Redirect RedirectData
          | TimeExceeded TimeData

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

   instance Enum Type where
         fromEnum (Redirect _) = 5
         fromEnum (TimeExceeded _) = 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 = RedirectData {redirectCode:: RedirectCode,
                         ip_addr:: Int, -- whatever
                         redirectData:: [Int]} -- or whatever

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

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

   data TimeExceededCode = 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) = fromEnum p: encode d
         encode p@(TimeExceeded d) = fromEnum p: encode d

   instance Encode RedirectData where
         encode d = fromEnum (redirectCode d): ip_addr d: redirectData d

   instance Encode TimeData where
         encode d = 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ón
--
Jón Fairbairn                                 [EMAIL PROTECTED]
31 Chalmers Road                                         [EMAIL PROTECTED]
Cambridge CB1 3SZ            +44 1223 570179 (after 14:00 only, please!)


_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell







      
-------------------------------------------------------------------------------------------------

      Save time by using an eTicket and our Self-Service Check-in Kiosks.
      For more information go to http://www.britishairways.com/eservice1


_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell