[Haskell-cafe] Simple GADTs, type families and type classes combination with type error.
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
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