[Haskell-cafe] Strange problem with type classes (ghc 6.8.2 looks
allright and ghc 6.10.1 doesn't).
Serguey Zefirov
sergueyz at gmail.com
Tue Sep 22 17:14:10 EDT 2009
I try to create yet another hardware description language embedded in
Haskell and faced a (perceived) bug in ghc 6.10.1 type checker. In ghc
6.8.2 everything works fine.
I need a type class that can express relationship between type and
its' "size in wires" (the number of bits needed to represent any value
of a type). The type class can be easily generalized to most haskell
data types and it's easy to write instance derivation using Template
Haskell.
I used multiparameter type classes because support for type families
in Template Haskell was incomplete in 6.10.1 and prior versions.
The source code below.
Do not forget to include -fcontext-stack=100 when trying to load the
code into ghci. The problem lines are between "THE PROBLEM!!"
comments.
Please, tell me, is it geniune bug or I misunderstand something about
Haskell type checker? How do you solve problems like that?
and, btw, you can take a look on how we can describe something
MIPS-alike in Haskell here: http://thesz.mskhug.ru/svn/hhdl/MIPS.hs
it is not finished by any means, but it gives a feel on how it will
look. I head to obtain (pretty) efficient simulation functions on
infinite streams (almost done, transformations are very simple) and
synthesable VHDL/Verilog description all from the same code that looks
like ordinary Haskell code.
-----------------------------------------------------------------------------------------------------------------------------
-- "A problem with functional dependencies.
-- use -fcontext-stack=100 ghc switch.
{-# LANGUAGE GADTs, FunctionalDependencies, MultiParamTypeClasses,
TypeSynonymInstances, FlexibleInstances, FlexibleContexts,
UndecidableInstances #-}
module Problem where
import Data.Bits
import Data.Word
-------------------------------------------------------------------------------
-- Type level arithmetic.
data Zero = Zero
data Succ n = Succ n
type ZERO = Zero
type ONE = Succ ZERO
type TWO = Succ ONE
type THREE = Succ TWO
type FOUR = Succ THREE
type FIVE = Succ FOUR
type SIX = Succ FIVE
type SEVEN = Succ SIX
type EIGHT = Succ SEVEN
type NINE = Succ EIGHT
type SIZE10 = Succ NINE
type SIZE11 = Succ SIZE10
type SIZE12 = Succ SIZE11
type SIZE13 = Succ SIZE12
type SIZE15 = Succ (Succ SIZE13)
type SIZE16 = Succ SIZE15
type SIZE20 = Succ (Succ (Succ (Succ (Succ SIZE15))))
type SIZE25 = Succ (Succ (Succ (Succ (Succ SIZE20))))
type SIZE26 = Succ SIZE25
type SIZE30 = Succ (Succ (Succ (Succ (Succ SIZE25))))
type SIZE32 = Succ (Succ SIZE30)
class Nat n where fromNat :: n -> Int
instance Nat Zero where fromNat = const 0
instance Nat n => Nat (Succ n) where fromNat ~(Succ n) = 1+fromNat n
class (Nat a, Nat b, Nat c) => CPlus a b c | a b -> c, a c -> b
--instance Nat a => CPlus a Zero a
instance Nat a => CPlus Zero a a
instance (CPlus a b c) => CPlus (Succ a) b (Succ c)
--instance (CPlus a b c) => CPlus (Succ a) b (Succ c)
--instance (CPlus a b c) => CPlus a (Succ b) (Succ c)
class (Nat a, Nat b, Nat c) => CMax a b c | a b -> c
instance CMax Zero Zero Zero
instance Nat a => CMax (Succ a) Zero (Succ a)
instance Nat a => CMax Zero (Succ a) (Succ a)
instance CMax a b c => CMax (Succ a) (Succ b) (Succ c)
class (Nat a, Nat b) => CDbl a b | a -> b
instance CPlus a a b => CDbl a b
class (Nat a, Nat b) => CPow2 a b | a -> b
instance CPow2 Zero (Succ Zero)
instance (CPow2 a b, CDbl b b2) => CPow2 (Succ a) b2
-------------------------------------------------------------------------------
-- Sized integer.
data IntSz n where
IntSz :: Nat sz => Integer -> IntSz sz
intSzSizeType :: IntSz n -> n; intSzSizeType _ = undefined
intSzSize :: Nat n => IntSz n -> Int; intSzSize n = fromNat $ intSzSizeType n
instance Nat sz => Eq (IntSz sz) where
(IntSz a) == (IntSz b) = a == b
instance Show (IntSz n) where
show n@(IntSz x) = show x++"{"++show (intSzSize n)++"}"
instance Nat sz => Num (IntSz sz) where
fromInteger x = IntSz x
(IntSz a) + (IntSz b) = IntSz $ a+b
(IntSz a) - (IntSz b) = IntSz $ a-b
(IntSz a) * (IntSz b) = IntSz $ a*b
abs = error "No abs for IntSz."
signum = error "No signum for IntSz."
-------------------------------------------------------------------------------
-- ToWires class, the main source of problems.
class Nat aSz => ToWires a aSz | a -> aSz where
wireSizeType :: a -> aSz
wireSizeType _ = undefined
-- size of a bus to hold a value in bits.
wireSize :: a -> Int
wireSize x = fromNat $ wireSizeType x
-- 2^wireSize, currently unused.
wireMul :: a -> Integer
wireMul x = Data.Bits.shiftL 1 (wireSize x)
-- selector size for decode (unused).
wireSelSize :: a -> Int
wireSelSize = const 0
-- Integer should occupy no more than wireSize bits, the remaining
bits should be 0
toWires :: a -> Integer
-- fromWires should work with integers that have non-zero bits
-- above wireSize index.
fromWires :: Integer -> a
-- enumeration.
-- valuesCount of (Maybe a) returns 1+valuesCount (x::a)
-- valuesCount of Either a b returns valuesCount (x::a) + valuesCount (yLLb)
-- valuesCount of (a,b) returns valuesCoutn (x::a) * valuesCount (y::b)
valuesCount :: a -> Integer
-- valueIndex.
-- get a value and return an index inside enumeration.
valueIndex :: a -> Integer
-------------------------------------------------------------------------------
-- Instances.
instance (ToWires x a,ToWires y b, CPlus a b c) => ToWires (x,y) c where
toWires (a,b) = Data.Bits.shiftL (toWires a) (wireSize b) .|. toWires b
fromWires x = (a,b)
where
b = fromWires x
a = fromWires $ Data.Bits.shiftR x (wireSize b)
valuesCount (a,b) = valuesCount a*valuesCount b
valueIndex (a,b) = valueIndex a*valuesCount b + valueIndex b
instance (ToWires x1 a,ToWires x2 b,ToWires x3 c,
CPlus b c bc, CPlus a bc abc) =>
ToWires (x1,x2,x3) abc where
toWires (a,b,c) = toWires (a,(b,c))
fromWires abc = (a,b,c)
where
(a,(b,c)) = fromWires abc
valuesCount (a,b,c) = valuesCount (a,(b,c))
valueIndex (a,b,c) = valueIndex (a,(b,c))
instance (ToWires x1 a,ToWires x2 b,ToWires x3 c,ToWires x4 d,ToWires x5 e,
CPlus d e de, CPlus c de cde, CPlus b cde bcde, CPlus a bcde abcde) =>
ToWires (x1,x2,x3,x4,x5) abcde where
toWires (a,b,c,d,e) = toWires (a,(b,(c,(d,e))))
fromWires abcde = (a,b,c,d,e)
where
(a,(b,(c,(d,e)))) = fromWires abcde
valuesCount (a,b,c,d,e) = valuesCount (a,(b,(c,(d,e))))
valueIndex (a,b,c,d,e) = valueIndex (a,(b,(c,(d,e))))
instance CPow2 FIVE size32 => ToWires Int size32 where
toWires n = fromIntegral n .&. 0xffffffff
fromWires x = fromIntegral x
valuesCount = const (Data.Bits.shiftL (1::Integer) 32)
valueIndex = fromIntegral
instance CPow2 FIVE size32 => ToWires Word32 size32 where
toWires n = fromIntegral n .&. 0xffffffff
fromWires x = fromIntegral x
valuesCount = const (Data.Bits.shiftL (1::Integer) 32)
valueIndex = fromIntegral
instance Nat size => ToWires (IntSz size) size where
toWires x@(IntSz n) = n .&. (Data.Bits.shiftL 1 (wireSize x) - 1)
fromWires x = fromIntegral x
valuesCount x = Data.Bits.shiftL (1::Integer) (wireSize x)
valueIndex x = toWires x
-------------------------------------------------------------------------------
-- Neccessary types for a problem.
-- A hack around bugs (??) in ghc 6.10.1.
data RI = RI (IntSz FIVE)
deriving (Eq,Show)
data Imm5 = Imm5 (IntSz FIVE)
deriving (Eq,Show)
data Imm16 = Imm16 (IntSz SIZE16)
deriving (Eq,Show)
data Imm26 = Imm26 (IntSz SIZE26)
deriving (Eq,Show)
instance ToWires RI FIVE where
toWires (RI x) = toWires x
fromWires x = RI $ fromWires x
valuesCount = const 32
valueIndex (RI x) = toWires x
instance ToWires Imm5 FIVE where
toWires (Imm5 x) = toWires x
fromWires x = Imm5 $ fromWires x
valuesCount = const 32
valueIndex (Imm5 x) = toWires x
instance ToWires Imm16 SIZE16 where
toWires (Imm16 x) = toWires x
fromWires x = Imm16 $ fromWires x
valuesCount (Imm16 x) = valuesCount x
valueIndex (Imm16 x) = valueIndex x
instance ToWires Imm26 SIZE26 where
toWires (Imm26 x) = toWires x
fromWires x = Imm26 $ fromWires x
valuesCount (Imm26 x) = valuesCount x
valueIndex (Imm26 x) = toWires x
instance ToWires a sz => ToWires (Maybe a) (Succ sz) where
toWires Nothing = 0
toWires (Just x) = shiftL (toWires x) 1 .|. 1
fromWires = undefined
valuesCount x = 1+valuesCount y
where
~(Just y) = x
valueIndex Nothing = 0
valueIndex (Just x) = 1+valueIndex x
-------------------------------------------------------------------------------
-- And a problem itself.
data Signed = Signed | Unsigned
deriving (Eq,Show)
data MIPSCmd regv =
Nop
| Trap
-- we mark destination register with RI. It never gets fetched.
-- we mark source registers as regv, because they can change their size
-- at FETCH stage (became Word32).
| AddU regv regv RI
| And regv regv RI
| Div Signed regv regv
deriving (Eq,Show)
instance ToWires Signed (Succ Zero) where
toWires (Signed) = Data.Bits.shiftL 0 1 .|. 0
toWires (Unsigned) = Data.Bits.shiftL 0 1 .|. 1
fromWires x = undefined
valuesCount x = 1 + (1 + 0)
where
~(Signed) = x
~(Unsigned) = x
valueIndex x = case x of
Signed -> 0 + 0
Unsigned -> (0 + 0) + 0
where
~(Signed) = x
~(Unsigned) = x
instance (ToWires regv_0 v_1, ToWires RI v_2,
CPlus v_1 v_1 vCPlus_3, CPlus vCPlus_3 v_2 vCPlus_4,
CPlus v_1 v_1 vCPlus_5, CPlus vCPlus_5 v_2 vCPlus_6,
ToWires Signed v_7, CPlus v_7 v_1 vCPlus_8, CPlus vCPlus_8 v_1 vCPlus_9,
CMax vCPlus_4 vCPlus_6 vCMax_10, CMax vCMax_10 vCPlus_9 vCMax_11)
=> ToWires (MIPSCmd regv_0) (Succ (Succ (Succ vCMax_11))) where
toWires (Nop) = Data.Bits.shiftL 0 3 .|. 0
toWires (Trap) = Data.Bits.shiftL 0 3 .|. 1
toWires (AddU a_12 a_13 a_14) =
Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL
(Data.Bits.shiftL 0 (wireSize a_12) .|. toWires a_12) (wireSize a_13)
.|. toWires a_13) (wireSize a_14) .|. toWires a_14) 3 .|. 2
toWires (And a_15 a_16 a_17) =
Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL
(Data.Bits.shiftL 0 (wireSize a_15) .|. toWires a_15) (wireSize a_16)
.|. toWires a_16) (wireSize a_17) .|. toWires a_17) 3 .|. 3
toWires (Div a_18 a_19 a_20) =
Data.Bits.shiftL (Data.Bits.shiftL (Data.Bits.shiftL
(Data.Bits.shiftL 0 (wireSize a_18) .|. toWires a_18) (wireSize a_19)
.|. toWires a_19) (wireSize a_20) .|. toWires a_20) 3 .|. 4
fromWires x = undefined
valuesCount x = 1 + (1 + ((valuesCount x_21 * (valuesCount x_22 *
(valuesCount x_23 * 1))) + ((valuesCount x_24 * (valuesCount x_25 *
(valuesCount x_26 * 1))) + ((valuesCount x_27 * (valuesCount x_28 *
(valuesCount x_29 * 1))) + 0))))
where
~(Nop) = x
~(Trap) = x
~(AddU x_21 x_22 x_23) = x
~(And x_24 x_25 x_26) = x
~(Div x_27 x_28 x_29) = x
-- Please don't mind that code is wrong, I can't get past typechecker here.
valueIndex x = case x of
Nop -> 0 + 0
Trap -> (0 + 0) + 0
-- THE PROBLEM!!!
AddU ax_30 ax_31 ax_32 ->
((0 + 0) + 0) + valueIndex (ax_32,(ax_30, ax_31))
-- /THE PROBLEM!!!
{-
And x_33 x_34 x_35 -> (((0 + 0) + 0)
+ valuesCount (x_32,
(x_30,
x_31))) + valueIndex (x_35,
(x_33,
x_34))
Div x_36 x_37 x_38 -> ((((0 + 0) + 0)
+ valuesCount (x_32,
(x_30,
x_31))) + valuesCount (x_35,
(x_33,
x_34))) + valueIndex (x_38,
(x_36,
x_37))
-}
where ~(Nop) = x
~(Trap) = x
~(AddU x_30 x_31 x_32) = x
~(And x_33 x_34 x_35) = x
~(Div x_36 x_37 x_38) = x
-----------------------------------------------------------------------------------------------------------------------------
More information about the Haskell-Cafe
mailing list