Re: [Haskell-cafe] Simple GADTs, type families and type classes combination with type error.
On Fri, Jul 22, 2011 at 12:12 PM, Serguey Zefirov sergu...@gmail.com wrote: Why does GHC complains on the code below ? (I'll explain in a second a requirement to do just so) I don't why =(. But you can workaround by using class CPU cpu where data CPUFunc cpu Note that you don't need the class constraint 'CPU cpu =' inside the GADT since 'cpu' is not an existential. Cheers, =) -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Simple GADTs, type families and type classes combination with type error.
On Fri, Jul 22, 2011 at 11:12 AM, Serguey Zefirov sergu...@gmail.com wrote:
-
{-# LANGUAGE GADTs, TypeFamilies #-}
class CPU cpu where
type CPUFunc cpu
data Expr cpu where
EVar :: String - Expr cpu
EFunc :: CPU cpu = CPUFunc cpu - Expr cpu
class CPU cpu = FuncVars cpu where
funcVars :: CPUFunc cpu - [String]
exprVars :: FuncVars cpu = Expr cpu - [String]
exprVars (EVar v) = [v]
-- an offending line:
exprVars (EFunc f) = funcVars f
-
I tried to split creation and analysis constraints. CPU required for
creation of expressions, FuncVars required for analysis. It all looks
nice but didn't work.
(In our real code EVar is slightly more complicated, featuring Var
cpu argument)
It looks like GHC cannot relate parameters inside and outside of
GADT constructor.
Not that I hesitate to add a method to a CPU class, but I think it is
not the right thing to do. So if I can split my task into two classes,
I will feel better.
GHC cannot decide what instance of FuncVars to use. The signature of
funcVars is:
funcVars :: FuncVars cpu = CPUFunc cpu - [String]
This does not take any arguments that allow cpu to be determined. For
instance, if there were instances (rolling them into one declaration
for simplicity):
instance FuncVars Int where
type CPUFunc Int = Int
...
instance FuncVars Char where
type CPUFunc Char = Int
Then GHC would see that CPUFunc cpu = Int, but from this, it cannot
determine whether cpu = Int or cpu = Char. CPUFunc is not
(necessarily) injective.
Making CPUFunc a data family as Felipe suggested fixes this by CPUFunc
essentially being a constructor of types, not a function that
computes. So it would be impossible for CPUFunc a = CPUFunc b unless a
= b.
Also, if you have a class whose only content is an associated type,
there's really no need for the class at all. It desugars into:
type family CPUFunc a :: *
class CPU a
So it's just a type family and an empty class, which will all have
exactly the same cases defined. You could instead use just the family.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Simple GADTs, type families and type classes combination with type error.
I just had a problem closely related to this on StackOverflow [1]
which was explained beautifully by cammcann.
The problem is that because type CPUFunc cpu is located inside the
definition of the class CPU it creates the illusion that they are
somehow tied together where CPUFunc is somehow in the CPU
namespace. It isn't. CPUFunc is actually defined globally and the
compiler would complain if you tried to create a CPUFunc type anywhere
else in your code.
The solution is the make CPUFunc a brand new datatype by changing
type CPUFunc cpu to data CPUFunc cpu .
-deech
[1]
http://stackoverflow.com/questions/6663547/writing-a-function-polymorphic-in-a-type-family
On Fri, Jul 22, 2011 at 10:12 AM, Serguey Zefirov sergu...@gmail.com wrote:
Why does GHC complains on the code below ? (I'll explain in a second a
requirement to do just so)
I get errors with ghc 6.12.1 and 7.0.2.
-
{-# LANGUAGE GADTs, TypeFamilies #-}
class CPU cpu where
type CPUFunc cpu
data Expr cpu where
EVar :: String - Expr cpu
EFunc :: CPU cpu = CPUFunc cpu - Expr cpu
class CPU cpu = FuncVars cpu where
funcVars :: CPUFunc cpu - [String]
exprVars :: FuncVars cpu = Expr cpu - [String]
exprVars (EVar v) = [v]
-- an offending line:
exprVars (EFunc f) = funcVars f
-
I tried to split creation and analysis constraints. CPU required for
creation of expressions, FuncVars required for analysis. It all looks
nice but didn't work.
(In our real code EVar is slightly more complicated, featuring Var
cpu argument)
It looks like GHC cannot relate parameters inside and outside of
GADT constructor.
Not that I hesitate to add a method to a CPU class, but I think it is
not the right thing to do. So if I can split my task into two classes,
I will feel better.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Simple GADTs, type families and type classes combination with type error.
2011/7/22 Dan Doel dan.d...@gmail.com: On Fri, Jul 22, 2011 at 11:12 AM, Serguey Zefirov sergu...@gmail.com wrote: GHC cannot decide what instance of FuncVars to use. The signature of funcVars is: funcVars :: FuncVars cpu = CPUFunc cpu - [String] This does not take any arguments that allow cpu to be determined. For instance, if there were instances (rolling them into one declaration for simplicity): instance FuncVars Int where type CPUFunc Int = Int ... instance FuncVars Char where type CPUFunc Char = Int Then GHC would see that CPUFunc cpu = Int, but from this, it cannot determine whether cpu = Int or cpu = Char. CPUFunc is not (necessarily) injective. But cpu variable is the same in all places. If we don't dive into CPUFunc reduction (to Int or whatever) we can safely match funcVars argument and unify cpu. This is the case when we write generic functions over type family application. Also, if you have a class whose only content is an associated type, there's really no need for the class at all. It desugars into: type family CPUFunc a :: * class CPU a It would be somewhat inconvenient. I omitted some constraints in CPU class for the sake of presentation. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Simple GADTs, type families and type classes combination with type error.
2011/7/22 Felipe Almeida Lessa felipe.le...@gmail.com: On Fri, Jul 22, 2011 at 12:12 PM, Serguey Zefirov sergu...@gmail.com wrote: Why does GHC complains on the code below ? (I'll explain in a second a requirement to do just so) I don't why =(. But you can workaround by using class CPU cpu where data CPUFunc cpu Thank you very much. I completely forgot that. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Simple GADTs, type families and type classes combination with type error.
On Fri, Jul 22, 2011 at 4:11 PM, Serguey Zefirov sergu...@gmail.com wrote: But cpu variable is the same in all places. If we don't dive into CPUFunc reduction (to Int or whatever) we can safely match funcVars argument and unify cpu. This is the case when we write generic functions over type family application. Here is approximately what the checking algorithm knows in the problematic case: exprVars (EFunc f) = funcVars f exprVars :: FuncVars cpu1 = Expr cpu1 - [String] EFunc f :: Expr cpu1 funcVars :: FuncVars cpu2 = CPUFunc cpu2 - [String] f :: CPUFunc cpu1 Thus, it can determine: CPUFunc cpu2 = CPUFunc cpu1 Now it needs to decide which instance of FuncVars to feed to funcVars. But it only knows that cpu2 should be such that the above type equation holds. However, since CPUFunc is a type family, it is not sound in general to reason from: CPUFunc cpu1 = CPUFunc cpu2 to: cpu1 = cpu2 So the type checker doesn't. You have nothing there that determines cpu1 to be the same as cpu2. So you need to make some change that does determine them to be the same. In situations like these, it would be handy if there were a way to specify what type certain variables are instantiated to, but it's sort of understandable that there isn't, because it'd be difficult to do in a totally satisfactory way. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
