[Haskell-beginners] Type polymorphism with size
Michael Snoyman
michael at snoyman.com
Tue Nov 18 17:18:46 EST 2008
On Tue, Nov 18, 2008 at 11:18 AM, Brent Yorgey <byorgey at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/beginners/attachments/20081118/8a75bca1/attachment-0001.htm
More information about the Beginners
mailing list