Haskell

Download

haskell@haskell.org

October 2004

89 participants
72 discussions

GHC / Hugs Disagree on Constraints
by Dominic Steinitz 02 Oct '04

02 Oct '04

GHC accepts this with -fglasgow-exts instance (Ord a, Bits a, Bounded a, Integral a, LargeWord a, Bits b, Bounded b, Integral b, LargeWord b) => Bounded (LargeKey a b) where minBound = 0 maxBound = fromIntegral $ (1 + fromIntegral (maxBound::b))* (1 + fromIntegral (maxBound::a)) - 1 Hugs rejects it with +N -98 with ERROR "Codec/Encryption/LargeKey.hs":94 - Cannot justify constraints in type annotation *** Expression : maxBound *** Type : b *** Given context : () *** Constraints : Bounded b Since I've already declared b to be Bounded, it looks like a bug in Hugs. Dominic. ======================================================================= module Codec.Encryption.LargeKey (Word128,Word192,Word256,LargeWord) where import Data.Word import Data.Bits import Numeric import Char -- Keys have certain capabilities. class LargeWord a where largeWordToInteger :: a -> Integer integerToLargeWord :: Integer -> a largeWordPlus :: a -> a -> a largeWordAnd :: a -> a -> a largeWordOr :: a -> a -> a largeWordShift :: a -> Int -> a largeWordXor :: a -> a -> a largeBitSize :: a -> Int -- Word64 is a key in the obvious way. instance LargeWord Word64 where largeWordToInteger = toInteger integerToLargeWord = fromInteger largeWordPlus = (+) largeWordAnd = (.&.) largeWordOr = (.|.) largeWordShift = shift largeWordXor = xor largeBitSize = bitSize -- Define larger keys from smaller ones. data LargeKey a b = LargeKey a b deriving (Eq, Ord) instance (Ord a, Bits a, LargeWord a, Bits b, LargeWord b) => LargeWord (LargeKey a b) where largeWordToInteger (LargeKey lo hi) = largeWordToInteger lo + (2^(bitSize lo)) * largeWordToInteger hi integerToLargeWord x = let (h,l) = x `quotRem` (2^(bitSize lo)) (lo,hi) = (integerToLargeWord l, integerToLargeWord h) in LargeKey lo hi largeWordPlus (LargeKey alo ahi) (LargeKey blo bhi) = LargeKey lo' hi' where lo' = alo + blo hi' = ahi + bhi + if lo' < alo then 1 else 0 largeWordAnd (LargeKey alo ahi) (LargeKey blo bhi) = LargeKey lo' hi' where lo' = alo .&. blo hi' = ahi .&. bhi largeWordOr (LargeKey alo ahi) (LargeKey blo bhi) = LargeKey lo' hi' where lo' = alo .|. blo hi' = ahi .|. bhi largeWordOr (LargeKey alo ahi) (LargeKey blo bhi) = LargeKey lo' hi' where lo' = alo .|. blo hi' = ahi .|. bhi largeWordXor (LargeKey alo ahi) (LargeKey blo bhi) = LargeKey lo' hi' where lo' = alo `xor` blo hi' = ahi `xor` bhi largeWordShift w 0 = w largeWordShift (LargeKey lo hi) x = if bitSize lo < bitSize hi then LargeKey (shift lo x) (shift hi x .|. (shift (conv lo) (x - (bitSize lo)))) else LargeKey (shift lo x) (shift hi x .|. (conv $ shift lo (x - (bitSize lo)))) where conv = integerToLargeWord . largeWordToInteger largeBitSize ~(LargeKey lo hi) = largeBitSize lo + largeBitSize hi instance (Ord a, Bits a, LargeWord a, Bits b, LargeWord b) => Show (LargeKey a b) where showsPrec p = showInt . largeWordToInteger instance (Ord a, Bits a, LargeWord a, Bits b, LargeWord b) => Num (LargeKey a b) where (+) = largeWordPlus fromInteger = integerToLargeWord -- Larger keys are instances of Bits provided their constituents are keys. instance (Ord a, Bits a, LargeWord a, Bits b, LargeWord b) => Bits (LargeKey a b) where (.&.) = largeWordAnd (.|.) = largeWordOr xor = largeWordXor shift = largeWordShift bitSize = largeBitSize instance (Ord a, Bits a, Bounded a, Integral a, LargeWord a, Bits b, Bounded b, Integral b, LargeWord b) => Bounded (LargeKey a b) where minBound = 0 maxBound = fromIntegral $ (1 + fromIntegral (maxBound::b))* (1 + fromIntegral (maxBound::a)) - 1 instance (Ord a, Bits a, LargeWord a, Ord b, Bits b, LargeWord b) => Integral (LargeKey a b) where toInteger = largeWordToInteger instance (Ord a, Bits a, LargeWord a, Ord b, Bits b, LargeWord b) => Real (LargeKey a b) instance Enum (LargeKey a b) type Word96 = LargeKey Word32 Word64 type Word128 = LargeKey Word64 Word64 type Word160 = LargeKey Word32 Word128 type Word192 = LargeKey Word64 Word128 type Word224 = LargeKey Word32 Word192 type Word256 = LargeKey Word64 Word192

1 0

Generalised algebraic data types
by Simon Peyton-Jones 01 Oct '04

01 Oct '04

Folks I've finished my first attempt at implementing Generalised Algebraic Data types in GHC. Ordinary algebraic data types are generalised to allow you to write an explicit type signature for each constructor; for example: data Term a where Lit :: Int -> Term Int Succ :: Term Int -> Term Int IsZero :: Term Int -> Term Bool If :: Term Bool -> Term a -> Term a -> Term a Notice that some of these constructors have return types that are not just "Term a"... that's the whole point! Now you can write typed evaluator for these terms: eval :: Term a -> a eval (Lit i) = i eval (Succ t) = 1 + eval t eval (IsZero i) = eval i == 0 eval (If b e1 e2) = if eval b then eval e1 else eval e2 GADTs are not a new idea. They go back to inductive type families in type theory and dependent types, and more recently have been studied in a programming-language context by Xi, Hinze & Cheney, Simonet & Pottier, and Sheard. Indeed, Tim Sheard's language Omega is has taken the same ideas a good deal further. He has a good bunch of links at his home page http://www.cs.pdx.edu/~sheard/ The only really new thing is that it's in GHC. Our paper about the ideas is at http://research.microsoft.com/~simonpj/papers/gadt/index.htm, and it has lots of references to related work. GADTs will be in GHC 6.4, which we'll release in the next month or two, but meanwhile it's in the HEAD of the CVS repository. Anyone who's prepared to build from source, or who can grab a development snapshot from the GHC website, can try it out. I'd like to encourage you to do so, so that you can discover the more egregious bugs before we ship 6.4, rather than after. (Also error messages are likely to be poor at first.) First-cut documentation of the feature is in ghc/docs; a typeset snapshot is at http://research.microsoft.com/~simonpj/tmp/gadt.html, There's a small collection of test programs that exercise GADTs in GHC's test suite: http://cvs.haskell.org/cgi-bin/cvsweb.cgi/fptools/testsuite/tests/ghc-re gress/gadt/ You can use these as a guide to syntax, and a source of programming ideas. You'll find red-black trees (invariants guaranteed by the types), evaluators, type checkers, and more besides. (NB: some are supposed to fail: see all.T. Most are transcribed from Tim's Omega examples.) I'd love to have more GADT tests: send them to me and I'll add them. And let me know how you get on. Simon

1 0