type refinement to a typeclass constrained type
Hello folks A section on GADTs in the GHC user's guide gives a simple example: data Term a where Lit :: Int -> Term Int Succ :: Term Int -> Term Int IsZero :: Term Int -> Term Bool eval :: Term a -> a eval (Lit i) = i eval (Succ t) = 1 + eval t eval (IsZero t) = eval t == 0 let's add Sum :: Term Int -> Term Int -> Term Int eval (Sum l r) = eval l + eval r it's ok But when I do this Sum :: (Num a) => Term a -> Term a -> Term a eval (Sum l r) = eval l + eval r --- same it doesn't typecheck with the error "no isntance Num a" writing eval (Sum (l::Num b => Term b) (r::Num b => Term b)) doesn't help. I wonder, if there's a way to do what I'm trying to do. After all, I'm allowed to declare Term that way. Or is this a restriction of type refinement?
Try the HEAD. GADTs + type classes are broken in 6.6., and will stay that way I'm afraid. Simon | -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of Daniil | Elovkov | Sent: 22 March 2007 17:12 | To: haskell-cafe@haskell.org | Subject: [Haskell-cafe] type refinement to a typeclass constrained type | | Hello folks | | A section on GADTs in the GHC user's guide gives a simple example: | | data Term a where | Lit :: Int -> Term Int | Succ :: Term Int -> Term Int | IsZero :: Term Int -> Term Bool | | eval :: Term a -> a | eval (Lit i) = i | eval (Succ t) = 1 + eval t | eval (IsZero t) = eval t == 0 | | let's add | Sum :: Term Int -> Term Int -> Term Int | eval (Sum l r) = eval l + eval r | | it's ok | | But when I do this | Sum :: (Num a) => Term a -> Term a -> Term a | eval (Sum l r) = eval l + eval r --- same | | it doesn't typecheck with the error "no isntance Num a" | | writing | eval (Sum (l::Num b => Term b) (r::Num b => Term b)) | doesn't help. | | I wonder, if there's a way to do what I'm trying to do. After all, I'm | allowed to declare Term that way. Or is this a restriction of type | refinement? | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe
Ok, thank you very much.
Interesting thing though, it's the same on 6.4.1.
Wasn't this brokenness introduced in 6.6, but rather has lingered in
ghc for a while, or since the introduction of GADTs, at all?
2007/3/22, Simon Peyton-Jones
Try the HEAD. GADTs + type classes are broken in 6.6., and will stay that way I'm afraid.
Simon
| -----Original Message----- | Wrom: HYUCDDJBLVLMHAALPTCXLYRWTQTIPWIGYOKSTTZRCLBDXRQBGJSNBOHMKHJYFMYXOEAIJJPHSCRTNHGSWZIDREXCAXZOWC | Elovkov | Sent: 22 March 2007 17:12 | To: haskell-cafe@haskell.org | Subject: [Haskell-cafe] type refinement to a typeclass constrained type | | Hello folks | | A section on GADTs in the GHC user's guide gives a simple example: | | data Term a where | Lit :: Int -> Term Int | Succ :: Term Int -> Term Int | IsZero :: Term Int -> Term Bool | | eval :: Term a -> a | eval (Lit i) = i | eval (Succ t) = 1 + eval t | eval (IsZero t) = eval t == 0 | | let's add | Sum :: Term Int -> Term Int -> Term Int | eval (Sum l r) = eval l + eval r | | it's ok | | But when I do this | Sum :: (Num a) => Term a -> Term a -> Term a | eval (Sum l r) = eval l + eval r --- same | | it doesn't typecheck with the error "no isntance Num a" | | writing | eval (Sum (l::Num b => Term b) (r::Num b => Term b)) | doesn't help. | | I wonder, if there's a way to do what I'm trying to do. After all, I'm | allowed to declare Term that way. Or is this a restriction of type | refinement? | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe
| Interesting thing though, it's the same on 6.4.1. | | Wasn't this brokenness introduced in 6.6, but rather has lingered in | ghc for a while, or since the introduction of GADTs, at all? No it's always been broken. I finally made GADTs and type classes work together in the HEAD a few months ago, using implication constraints for the first time.
Ok,
btw, this works :)
data Cnd c where
In :: (Eq (c a)) => c a -> [c a] -> Cnd c
check :: (Eq (c a)) => Cnd c -> Bool
check (x `In` items) = x `elem` items
That's nice :)
2007/3/23, Simon Peyton-Jones
| Interesting thing though, it's the same on 6.4.1. | | Wasn't this brokenness introduced in 6.6, but rather has lingered in | ghc for a while, or since the introduction of GADTs, at all?
No it's always been broken. I finally made GADTs and type classes work together in the HEAD a few months ago, using implication constraints for the first time.
participants (2)
-
Daniil Elovkov -
Simon Peyton-Jones