Dependent Types

[Dominic Steinitz]

I've managed to crack something that always annoyed me when I used to do
network programming. However, Hugs and GHC behave differently. I'd be
interested in views on this approach and also which implementation behaves
correctly.

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. Here's a way I came up with for checking
at compile time in Haskell.

module Main(main) where

-- ICMP has many more values for the type byte but we only need two for the
example.

data Redirect = Redirect
data TimeExceeded = TimeExceeded

data ICMPType = MkRedirect Redirect
              | MkTimeExceeded TimeExceeded

-- 5 and 11 are the values that get sent.

instance Enum ICMPType where
  fromEnum (MkRedirect Redirect) = 5
  fromEnum (MkTimeExceeded TimeExceeded) = 11

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

data ICMPCodeTimeExceeded = ExcTTL
                          | ExcFragTime
   deriving Enum

class Encode a b | a -> b where
   encode :: a -> b

instance Encode ICMPType String where
   encode = show . fromEnum

instance Encode Redirect (ICMPCodeRedirect -> String) where
   encode a y = encode (MkRedirect a) ++ (show (fromEnum y))

instance Encode TimeExceeded (ICMPCodeTimeExceeded -> String) where
   encode b z = encode (MkTimeExceeded b) ++ (show (fromEnum z))

Now I can say things like

encode Redirect Redir

and get the value "50". But if I say

encode Redirect ExcTTL then I get a type error. GHC gives

Couldn't match `ICMPCodeRedirect' against `ICMPCodeTimeExceeded'
    Expected type: ICMPCodeRedirect -> String
    Inferred type: ICMPCodeTimeExceeded -> t

and Hugs gives

ERROR: Constraints are not consistent with functional dependency
*** Constraint       : Encode Redirect (ICMPCodeTimeExceeded -> [Char])
*** And constraint   : Encode Redirect (ICMPCodeRedirect -> String)
*** For class        : Encode a b
*** Break dependency : a -> b

This is just what you want as it picks up errors at compile time not at run
time.

However, if I now comment out the functional dependency

class Encode a b {- | a -> b -} where
   encode :: a -> b

and include the expressions

x = encode TimeExceeded ExcTTL

main = putStrLn x

then Hugs complains

ERROR "codes.hs" (line 37): Unresolved top-level overloading
*** Binding             : x
*** Outstanding context : Encode TimeExceeded (ICMPCodeTimeExceeded -> b)

whereas GHC doesn't complain.

Which is right?

Dominic.