On Tue, Nov 18, 2008 at 11:18 AM, Brent Yorgey <byorgey@seas.upenn.edu> wrote:
Hm, interesting!  The problem is that 'get' does not take any
arguments, so must determine what to do from the type at which it is
called.  So the number of words to be read needs to be in the type.
We can't put actual Int values in a type -- but there is actually a
way to do what you want, by encoding natural numbers at the type
level!  I don't know whether this really belongs on a 'beginners' list
but I couldn't resist. =)


data Z      -- the type representing zero
data S n    -- the type representing the successor of another natural

-- for example,  Z,  S Z,  and S (S Z)  are types representing
--   zero, one, and two.

-- the n is for a type-level natural representing the length of the list.
data MFChar n = MFChar [Word8]

-- add a Word8 to the beginning of an MFChar, resulting in an MFChar
--   one word longer
mfCons :: Word8 -> MFChar n -> MFChar (S n)
mfCons w (MFChar ws) = MFChar (w:ws)

instance Binary (MFChar Z) where
 get = return $ MFChar []

instance (Binary (MFChar n)) => Binary (MFChar (S n)) where
 get = do ebcdic <- getWord8
          rest   <- get    -- the correct type of get is
                           -- inferred due to the use of mfCons below
          return $ mfCons (ebcdicToAscii ebcdic) rest


Now if you wanted to read a field with 20 chars, you can use

 get :: Get (MFChar (S (S (S ... 20 S's ... Z))))

Ugly, I know. You could make it slightly more bearable by defining
some type synonyms at the top of your program like

 type Five = S (S (S (S (S Z))))
 type Ten = S (S (S (S (S Five))))

and so on.  Then you can just say   get :: Get (MFChar Ten) or whatever.

This is untested but it (or something close to it) ought to work.  Of
course, you may well ask yourself whether this contortion is really
worth it.  Maybe it is, maybe it isn't, but I can't think of a better
way to do it in Haskell.  In a dependently typed language such as
Agda, we could just put regular old natural numbers in the types,
instead of going through contortions to encode natural numbers as
types as we have to do here.  So I guess the real answer to your
question is "use a dependently typed language". =)

If you have problems getting this to work or more questions, feel free
to ask!

Very interesting solution to the problem. I tried it out and it works perfectly... but it's just too much of a hack for my tastes (no offense; I think it was very cool). I thought about it a bit and realized what I really want is a way to deal with tuples of the same type, which led to this kind of implementation.

class RepTuple a b | a -> b where
    toList :: a -> [b]
    tMap :: (b -> b) -> a -> a

instance RepTuple (a, a) a where
    toList (a, b) = [a, b]
    tMap f (a, b) = (f a, f b)

And so on and so forth for every kind of tuple. Of course, this runs into the issue of the single case, for which I used the OneTuple library (actually, I wrote my own right now, but I intend to just use the OneTuple library).

I can then do something like this (which I have tested and works):

data MFChar w = MFChar w
    deriving Eq
instance (RepTuple w a, Integral a) => Show (MFChar w) where
    show (MFChar ws) = map (chr . fromIntegral) $ toList ws
instance (Integral a, Binary w, RepTuple w a) => Binary (MFChar w) where
    put = undefined
    get = do ebcdic <- get
             let ascii = tMap ebcdicToAscii ebcdic
             return $ MFChar ascii

type MFChar1 = MFChar (OneTuple Word8)
type MFChar2 = MFChar (Word8, Word8)
type MFChar4 = MFChar (Word8, Word8, Word8, Word8)
type MFChar5 = MFChar (Word8, Word8, Word8, Word8, Word8)
type MFChar10 = MFChar (Word8, Word8, Word8, Word8, Word8,
                        Word8, Word8, Word8, Word8, Word8)

If I wanted, I could do away with the tMap function and just include the ebcdicToAscii step in the show instance.

Michael