Simple GADTs, type families and type classes combination with type error.

older
Wrong Answer in SPOJ 6044. Minimum...

Serguey Zefirov

22 Jul 2011 22 Jul '11

11:12 a.m.

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.

Show replies by date

Felipe Almeida Lessa

22 Jul 22 Jul

11:21 a.m.

New subject: Simple GADTs, type families and type classes combination with type error.

On Fri, Jul 22, 2011 at 12:12 PM, Serguey Zefirov 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.

Serguey Zefirov

4:12 p.m.

New subject: Simple GADTs, type families and type classes combination with type error.

2011/7/22 Felipe Almeida Lessa :

...

On Fri, Jul 22, 2011 at 12:12 PM, Serguey Zefirov 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.

Dan Doel

11:32 a.m.

New subject: Simple GADTs, type families and type classes combination with type error.

On Fri, Jul 22, 2011 at 11:12 AM, Serguey Zefirov 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

Serguey Zefirov

4:11 p.m.

New subject: Simple GADTs, type families and type classes combination with type error.

2011/7/22 Dan Doel :

...

On Fri, Jul 22, 2011 at 11:12 AM, Serguey Zefirov 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.

Dan Doel

5:43 p.m.

New subject: Simple GADTs, type families and type classes combination with type error.

On Fri, Jul 22, 2011 at 4:11 PM, Serguey Zefirov 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

aditya siram

12:15 p.m.

New subject: 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... On Fri, Jul 22, 2011 at 10:12 AM, Serguey Zefirov 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

5053

Age (days ago)

5053

Last active (days ago)

List overview

Download

6 comments

4 participants

participants (4)

aditya siram
Dan Doel
Felipe Almeida Lessa
Serguey Zefirov