From Functional Dependencies to Type Families
{-# OPTIONS -fglasgow-exts #-}
module VarArg where import Data.FiniteMap -- for an example below
class BuildList a r | r-> a where build' :: [a] -> a -> r
instance BuildList a [a] where build' l x = reverse$ x:l
instance BuildList a r => BuildList a (a->r) where build' l x y = build'(x:l) y
--build :: forall r a. (BuildList a r) => a -> r build x = build' [] x
I'm trying to replace the code below to work with type families, I started out replacing the definition of class with : class BuildList r where type Build r build' :: [Build r] -> Build r -> r follow by the instance for [a] resulting in instance BuildList [a] where type Build [a] = a build' l x = reverse $ x:l Until here, everything is working, and I'm able to do
build' [2,3,4] 1 :: [Integer] [4,3,2,1]
then I move on to the next instance (a -> r) with instance BuildList r => BuildList (a-> r) where type Build (a -> r) = a build' l x = \ y -> build'(x:l) y But I get the following error Couldn't match expected type `Build r' against inferred type `a' `a' is a rigid type variable bound by the instance declaration at /home/adolfo/foo.hs:347:35 In the first argument of `(:)', namely `x' In the first argument of `build'', namely `(x : l)' In the expression: build' (x : l) y then I try with : instance BuildList r => BuildList (a-> r) where type Build (a -> r) = Build r build' l x = \ y -> build'(x:l) y And I get Couldn't match expected type `a' against inferred type `Build r' `a' is a rigid type variable bound by the instance declaration at /home/adolfo/foo.hs:347:35 Expected type: [Build r] Inferred type: [Build (a -> r)] In the second argument of `(:)', namely `l' In the first argument of `build'', namely `(x : l)' I have been trying to figure out, which type should it be, but I haven't found the correct one, any ideas ? Thanks - Adolfo Builes
{-# OPTIONS -fglasgow-exts #-}
module VarArg where import Data.FiniteMap -- for an example below
class BuildList a r | r-> a where build' :: [a] -> a -> r
instance BuildList a [a] where build' l x = reverse$ x:l
instance BuildList a r => BuildList a (a->r) where build' l x y = build'(x:l) y
--build :: forall r a. (BuildList a r) => a -> r build x = build' [] x
I'm trying to replace the code below to work with type families, I started out replacing the definition of class with : class BuildList r where type Build r build' :: [Build r] -> Build r -> r follow by the instance for [a] resulting in instance BuildList [a] where type Build [a] = a build' l x = reverse $ x:l Until here, everything is working, and I'm able to do
build' [2,3,4] 1 :: [Integer] [4,3,2,1]
then I move on to the next instance (a -> r) with instance BuildList r => BuildList (a-> r) where type Build (a -> r) = a build' l x = \ y -> build'(x:l) y But I get the following error Couldn't match expected type `Build r' against inferred type `a' `a' is a rigid type variable bound by the instance declaration at /home/adolfo/foo.hs:347:35 In the first argument of `(:)', namely `x' In the first argument of `build'', namely `(x : l)' In the expression: build' (x : l) y then I try with : instance BuildList r => BuildList (a-> r) where type Build (a -> r) = Build r build' l x = \ y -> build'(x:l) y And I get Couldn't match expected type `a' against inferred type `Build r' `a' is a rigid type variable bound by the instance declaration at /home/adolfo/foo.hs:347:35 Expected type: [Build r] Inferred type: [Build (a -> r)] In the second argument of `(:)', namely `l' In the first argument of `build'', namely `(x : l)' I have been trying to figure out, which type should it be, but I haven't found the correct one, any ideas ? Thanks - Adolfo Builes
Hi Adolfo This is quite a tricky one and I haven't got a proper answer (hopefully someone will come along with one soon). But I've an initial observation: Longhand (i.e. without the type class - but relying on previously defined instances) the type family version of buildlist on functions is: buildList_fun l x = \y -> build' (x:l) y Asking for the type at the GHCi prompt gives: buildList_fun :: (BuildList r) => [Build r] -> Build r -> Build r -> r Whereas for the fun dep version build_fun l x y = build' (x:l) y The type is: build_fun :: (BuildList a r) => [a] -> a -> a -> r Crucially the last part of the type is r. Why you can't type your TF version seems to be because the answer type of the continuation is fixed to a not r. (the fun dep version is also a multi parameter class so you are allowed a different answer type). [I'm calling out to the gallery for help at this point!]. Best wishes Stephen
Am Donnerstag 03 Dezember 2009 04:06:43 schrieb Adolfo Builes:
{-# OPTIONS -fglasgow-exts #-}
module VarArg where import Data.FiniteMap -- for an example below
class BuildList a r | r-> a where build' :: [a] -> a -> r
instance BuildList a [a] where build' l x = reverse$ x:l
instance BuildList a r => BuildList a (a->r) where build' l x y = build'(x:l) y
--build :: forall r a. (BuildList a r) => a -> r build x = build' [] x
I'm trying to replace the code below to work with type families, I started out replacing the definition of class with :
class BuildList r where type Build r build' :: [Build r] -> Build r -> r
follow by the instance for [a] resulting in
instance BuildList [a] where type Build [a] = a build' l x = reverse $ x:l
Until here, everything is working, and I'm able to do
build' [2,3,4] 1 :: [Integer] [4,3,2,1]
then I move on to the next instance (a -> r) with
instance BuildList r => BuildList (a-> r) where type Build (a -> r) = a build' l x = \ y -> build'(x:l) y
But I get the following error
Couldn't match expected type `Build r' against inferred type `a' `a' is a rigid type variable bound by the instance declaration at /home/adolfo/foo.hs:347:35 In the first argument of `(:)', namely `x' In the first argument of `build'', namely `(x : l)' In the expression: build' (x : l) y
then I try with :
instance BuildList r => BuildList (a-> r) where type Build (a -> r) = Build r build' l x = \ y -> build'(x:l) y
And I get
Couldn't match expected type `a' against inferred type `Build r' `a' is a rigid type variable bound by the instance declaration at /home/adolfo/foo.hs:347:35 Expected type: [Build r] Inferred type: [Build (a -> r)] In the second argument of `(:)', namely `l' In the first argument of `build'', namely `(x : l)'
I have been trying to figure out, which type should it be, but I haven't found the correct one, any ideas ?
I think instance (BuildList r, Build r ~ a) => BuildList (a -> r) where type Build (a -> r) = a build' l x = \y -> build' (x:l) y should work. You need to tell the compiler explicitly that a and Build r should be the same type.
Thanks
- Adolfo Builes
You need to tell the compiler explicitly that a and Build r should be the same type.
Thanks Daniel :). That was the trick .
It's the first time that I see "~", is that from -XUndecidableInstances ? .
Also, thanks to Stephen.
-
Adolfo
On Dec 3, 2009 6:30am, Daniel Fischer
Am Donnerstag 03 Dezember 2009 04:06:43 schrieb Adolfo Builes:
{-# OPTIONS -fglasgow-exts #-}
module VarArg where
import Data.FiniteMap -- for an example below
class BuildList ar | r-> a where
build' :: [a] -> a -> r
instance BuildList a [a] where
build' lx = reverse$ x:l
instance BuildList ar => BuildList a (a->r) where
build' lxy = build'(x:l) y
--build :: forall r a. (BuildList ar) => a -> r
build x = build' [] x
I'm trying to replace the code below to work with type families, I started
out replacing the definition of class with :
class BuildList r where
type Build r
build' :: [Build r] -> Build r -> r
follow by the instance for [a] resulting in
instance BuildList [a] where
type Build [a] = a
build' lx = reverse $ x:l
Until here, everything is working, and I'm able to do
build' [2,3,4] 1 :: [Integer]
[4,3,2,1]
then I move on to the next instance (a -> r) with
instance BuildList r => BuildList (a-> r) where
type Build (a -> r) = a
build' lx = \ y -> build'(x:l) y
But I get the following error
Couldn't match expected type `Build r' against inferred type `a'
`a' is a rigid type variable bound by
the instance declaration at /home/adolfo/foo.hs:347:35
In the first argument of `(:)', namely `x'
In the first argument of `build'', namely `(x : l)'
In the expression: build' (x : l) y
then I try with :
instance BuildList r => BuildList (a-> r) where
type Build (a -> r) = Build r
build' lx = \ y -> build'(x:l) y
And I get
Couldn't match expected type `a' against inferred type `Build r'
`a' is a rigid type variable bound by
the instance declaration at /home/adolfo/foo.hs:347:35
Expected type: [Build r]
Inferred type: [Build (a -> r)]
In the second argument of `(:)', namely `l'
In the first argument of `build'', namely `(x : l)'
I have been trying to figure out, which type should it be, but I haven't
found the correct one, any ideas ?
I think
instance (BuildList r, Build r ~ a) => BuildList (a -> r) where
type Build (a -> r) = a
build' lx = \y -> build' (x:l) y
should work.
You need to tell the compiler explicitly that a and Build r should be the same type.
Thanks
-
Adolfo Builes
Am Donnerstag 03 Dezember 2009 19:51:31 schrieb builes.adolfo@googlemail.com:
You need to tell the compiler explicitly that a and Build r should be the same type.
Thanks Daniel :). That was the trick .
It's the first time that I see "~", is that from -XUndecidableInstances ? .
No, it's part of the TypeFamilies extension. http://www.haskell.org/haskellwiki/GHC/Type_families#Equality_constraints and http://www.haskell.org/ghc/docs/latest/html/users_guide/type-families.html (much overlap). It requires UndecidableInstances ( http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class- extensions.html#undecidable-instances ) because both type variables from the instance head appear in the constraints, so the compiler can't prove that type inference will terminate. You tell it that you think it will terminate, and it goes forth. Which reminds me:
{-# OPTIONS -fglasgow-exts #-}
is deprecated. Use LANGUAGE pragmas, in this case {-# LANGUAGE TypeFamilies, UndecidableInstances #-} ({-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} for the FunDep version).
participants (4)
-
Adolfo Builes -
builes.adolfo＠googlemail.com
-
Daniel Fischer -
Stephen Tetley