I think your problem here is that there's no mention of `a' on the left-hand size of from_val's type signature; you either need to use MPTC+fundep to associate what result is compared to a, or else use a phantom type parameter of Val to make it "data Val result a = ..." and then "from_val :: Val result a -> Maybe a".

Aha! Why didn't I think of "plain" old MPTC+fundep? For some reason type families feel a lot more fun. Turns out you can write 'instance Typecheck (SomeMonad result) result' and instead of complaining about a duplicate symbol it unifies 'result', exactly like I wanted. It appears to work like a charm, thanks so much! Though it says it fails the Coverage Condition and I need UndecidableInstances...

I'm interested in situations where you think fundeps work and type families don't.  Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs).

If you think you have such as case, do send me a test case.

Well, from looking at the documentation, it looks like I could maybe use a type family if I could write: class (DerivedOf a ~ derived) => Typecheck a derived where ... Presumably then I could combine functions 'Typecheck a derived' constraints without getting lots of "Could not deduce (Typecheck a derived3) from the context (Typecheck a derived13)" errors. I'm only guessing though, because it looks like it's not implemented yet as of 6.12.3. So is your question whether I have a use case for fundeps supposing equality constraints in superclass contexts were implemented and they do what I hope they do, or is it do I have a use for those equality constraints as a motivation to implement them? In either case, I can give you some code that works with mptc+fundep but not with type families, unless I'm not using type families correctly of course. But if the type equality thing is coming regardless, then I can just wait for 6.14 or whatever and switch over then.

I'm interested in situations where you think fundeps work and type families don't. Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs).

If you think you have such as case, do send me a test case.

Do you have a wiki page somewhere collecting these examples? I seem to recall that similar discussions have arisen before and test cases have been provided but I wouldn't know where to check for the currently recorded state of differences. Also, what is the difference between fundeps and type families wrt local type constraints? I had always assumed them to be equivalent, if fully implemented. Similar to logic vs functional programming, where Haskellers tend to find the latter more convenient. Functional logic programming shows that there are some tricks missing if one just drops the logic part. Claus

On Thu, Jul 1, 2010 at 7:54 PM, Simon Peyton-Jones wrote:

| Also, what is the difference between fundeps and type families | wrt local type constraints? I had always assumed them to be | equivalent, if fully implemented. Similar to logic vs functional | programming, where Haskellers tend to find the latter more | convenient. Functional logic programming shows that there | are some tricks missing if one just drops the logic part.

Until now, no one has know how to combine fundeps and local constraints. For example

class C a b | a->b where op :: a -> b

instance C Int Bool where op n = n>0

data T a where T1 :: T a T2 :: T Int

-- Does this typecheck? f :: C a b => T a -> Bool f T1 = True f T2 = op 3

The function f "should" typecheck because inside the T2 branch we know that (a~Int), and hence by the fundep (b~Bool). But we have no formal type system for fundeps that describes this, and GHC's implementation certainly rejects it.

Martin Sulzmann, Jeremy Waznyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wazny:Jeremy.h..., Peter J. Stuckeyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/s/Stuckey:Peter_...: A Framework for Extended Algebraic Data Types. FLOPS 2006http://www.informatik.uni-trier.de/%7Eley/db/conf/flops/flops2006.html#Sulzm...: 47-64 describes such a system, fully implemented in Chameleon, but this system is no longer maintained. Type families and Fundeps are equivalent in expressive power and it's not too hard to show how to encode one in terms of the other. Local constraints are an orthogonal extension. In terms of type inference, type families + local constraints and fundeps + local constraints pose the same challenges. Probably, Simon is refrerring to the 'unresolved' issue of providing a System F style translation for fundeps + local constraints. Well, the point is that System FC is geared toward type families. The two possible solutions are (a) either consider fundeps as syntactic sugar for type families (doesn't quite work once you throw in overlapping instances), (b) design a variant System FC_fundep which has built-in support for fundeps. -Martin

Simon Peyton-Jones wrote:

Until now, no one has know how to combine fundeps and local constraints. For example

class C a b | a->b where op :: a -> b

instance C Int Bool where op n = n>0

data T a where T1 :: T a T2 :: T Int

-- Does this typecheck? f :: C a b => T a -> Bool f T1 = True f T2 = op 3

The function f "should" typecheck because inside the T2 branch we know that (a~Int), and hence by the fundep (b~Bool). But we have no formal type system for fundeps that describes this, and GHC's implementation certainly rejects it.

At least for this particular example, a simple desugaring translation makes even GHC 6.10.4 accept the example. We first desugar GADT into the regular ADT and the EQ constraint (the process, as I understand, already happens under the hood). We then make use of that constraint.

{-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-}

module F where

class C a b | a->b where op :: a -> b

instance C Int Bool where op n = n>0

data EQ a b where Refl :: EQ a a

-- A primitive version of Leibniz substitution principle. cast :: EQ a b -> a -> b cast Refl x = x

-- Original GADT -- data T a where -- T1 :: T a -- T2 :: T Int

-- desugared version of T data TT a = TT1 | TT2 (EQ a Int)

g :: C a b => TT a -> Bool g TT1 = True g (TT2 eq) = op (if False then cast eq undefined else 3)

test1 = g (TT2 Refl)

It works. Martin Sulzmann wrote:

Type families and Fundeps are equivalent in expressive power and it's not too hard to show how to encode one in terms of the other.

As Martin himself said in the next paragraph of his message, the equivalence claim has an exception: overlapping instances. Functional dependencies do work with overlapping instances, but type families do not. That issue has been noted just the other month on this list. There is another exception. Let's consider type class C with a functional dependency, and a seemingly equivalent type family F.

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes, FunctionalDependencies #-}

module F1 where

class C a b | a->b instance C Int Bool

type family F a :: * type instance F Int = Bool

newtype N1 a = N1 (F a)

n1 :: N1 Int -> Bool n1 (N1 x) = x

t1 = n1 (N1 True)

newtype N2 a = N2 (forall b. C a b => b)

n2 :: N2 Int -> Bool n2 (N2 x) = x

-- t2 = n2 ((N2 True) :: N2 Int)

The code type checks. It seems that for each piece of code using C we can write an equivalent piece of code using F -- until we come to t1 and t2. If we uncomment the last line, we get a type error /tmp/c.hs:25:13: Couldn't match expected type `b' against inferred type `Bool' `b' is a rigid type variable bound by the polymorphic type `forall b. (C Int b) => b' at /tmp/c.hs:25:10 In the first argument of `N2', namely `True' In the first argument of `n2', namely `((N2 True) :: N2 Int)' In the expression: n2 ((N2 True) :: N2 Int) Although the type variable b must be Bool (since it is uniquely determined by the functional dependency C Int b), GHC can't see that.

f :: forall a b. C a b => T a -> Bool f T1 = True f T2 = (op :: a -> b) 3

as that results in the counter-intuitive

Couldn't match expected type `Bool' against inferred type `b' `b' is a rigid type variable bound by the type signature for `f' at C:\Users\claus\Desktop\tmp\fd-local.hs:17:14 In the expression: (op :: a -> b) 3 In the definition of `f': f T2 = (op :: a -> b) 3

Which seems to be a variant of Oleg's example?

If it is, it is a simpler variant, because it has a workaround: f :: forall a b. C a b => T a -> Bool f T1 = True f T2 = (op :: C a b1 => a -> b1) 3 While playing around with Oleg's example, I also found the following two pieces (still ghc-6.12.3): -- first, a wonderful error message instead of expected simplification Prelude> (id :: (forall b. b~Bool=>b->b) -> (forall b. b~Bool=>b->b)) <interactive>:1:1: Couldn't match expected type `forall b. (b ~ Bool) => b -> b' against inferred type `forall b. (b ~ Bool) => b -> b' Expected type: forall b. (b ~ Bool) => b -> b Inferred type: forall b. (b ~ Bool) => b -> b In the expression: (id :: (forall b. (b ~ Bool) => b -> b) -> (forall b. (b ~ Bool) => b -> b)) In the definition of `it': it = (id :: (forall b. (b ~ Bool) => b -> b) -> (forall b. (b ~ Bool) => b -> b)) -- second, while trying the piece with classic, non-equality constraints Prelude> (id :: (forall b. Eq b=>b->b) -> (forall b. Eq b=>b->b)) <interactive>:1:0: No instance for (Show ((forall b1. (Eq b1) => b1 -> b1) -> b -> b)) arising from a use of `print' at <interactive>:1:0-55 Possible fix: add an instance declaration for (Show ((forall b1. (Eq b1) => b1 -> b1) -> b -> b)) In a stmt of an interactive GHCi command: print it Note that the second version goes beyond the initial problem, to the missing Show instance, but the error message loses the Eq constraint on b! -- it is just the error message, the type is still complete Prelude> :t (id :: (forall b. Eq b=>b->b) -> (forall b. Eq b=>b->b)) (id :: (forall b. Eq b=>b->b) -> (forall b. Eq b=>b->b)) :: (Eq b) => (forall b1. (Eq b1) => b1 -> b1) -> b -> b I don't have a GHC head at hand, perhaps that is doing better? Claus

Prelude> :t id :: Eq b => b -> b id :: Eq b => b -> b :: (Eq b) => b -> b Prelude> id :: Eq b => b -> b

<interactive>:1:0: No instance for (Show (b -> b)) arising from a use of `print' at <interactive>:1:0-19 Possible fix: add an instance declaration for (Show (b -> b)) In a stmt of a 'do' expression: print it

The Eq constraint is irrelevant to the fact that there is no b -> b Show instance. The search for an instance looks only at the type part, and if it finds a suitable match, then checks if the necessary constraints are also in place.

Thanks - that first sentence is right, but not because of the second!-) I thought the error message was misleading, speaking of instance when it should have been speaking about instance *head*. But I was really confused by the difference between (making the show explicit and using scoped type variables): *Main> :t (show (id::a->a))::forall a.Eq a=>String <interactive>:1:0: Ambiguous constraint `Eq a' At least one of the forall'd type variables mentioned by the constraint must be reachable from the type after the '=>' In an expression type signature: forall a. (Eq a) => String In the expression: (show (id :: a -> a)) :: forall a. (Eq a) => String <interactive>:1:1: Could not deduce (Show (a -> a)) from the context (Eq a) arising from a use of `show' at <interactive>:1:1-15 Possible fix: add (Show (a -> a)) to the context of an expression type signature or add an instance declaration for (Show (a -> a)) In the expression: (show (id :: a -> a)) :: forall a. (Eq a) => String which does list a non-empty context from which 'Show (a->a)' could not be deduced and *Main> :t show (id :: Eq a => a-> a) <interactive>:1:0: No instance for (Show (a -> a)) arising from a use of `show' at <interactive>:1:0-25 Possible fix: add an instance declaration for (Show (a -> a)) In the expression: show (id :: (Eq a) => a -> a) which only talks about general 'Show (a->a)' instances. We cannot define 'instance Show (forall a. Eq a=>a->a)', which is why the 'Eq a' constraint plays no role, I think.. Btw, the issues in the other example can be made more explicit by defining: class MyEq a b | a->b, b->a instance MyEq a a First, both FDs and TFs simplify this: *Main> :t id :: (forall b. MyEq b Bool => b->b) id :: (forall b. MyEq b Bool => b->b) :: Bool -> Bool *Main> :t id :: (forall b. b~Bool => b->b) id :: (forall b. b~Bool => b->b) :: Bool -> Bool but the FD version here typechecks (note, though, that the type is only partially simplified) *Main> :t id :: (forall b. MyEq b Bool => b->b) -> (forall b. MyEq b Bool => b->b) id :: (forall b. MyEq b Bool => b->b) -> (forall b. MyEq b Bool => b->b) :: (forall b. (MyEq b Bool) => b -> b) -> Bool -> Bool while the TF version doesn't *Main> :t id :: (forall b. b~Bool => b->b) -> (forall b. b~Bool => b->b) <interactive>:1:0: Couldn't match expected type `forall b. (b ~ Bool) => b -> b' against inferred type `forall b. (b ~ Bool) => b -> b' Expected type: forall b. (b ~ Bool) => b -> b Inferred type: forall b. (b ~ Bool) => b -> b In the expression: id :: (forall b. (b ~ Bool) => b -> b) -> (forall b. (b ~ Bool) => b -> b) Claus

Simon Peyton-Jones wrote:

I'm interested in situations where you think fundeps work and type families don't. Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs).

If you think you have such as case, do send me a test case.

As an example, is it possible to implement something like: http://okmij.org/ftp/Haskell/deepest-functor.lhs with TF only? I believe the following wiki-page http://www.haskell.org/haskellwiki/GHC/AdvancedOverlap also points out that "However, there's a problem: overlap is not allowed at all for type families!!" (c) or is it just a question of implementing closed type families? -- View this message in context: http://old.nabble.com/checking-types-with-type-families-tp28967503p29049813.... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

On Sat, Jul 3, 2010 at 3:32 AM, Kevin Quick wrote:

On Wed, 23 Jun 2010 00:14:03 -0700, Simon Peyton-Jones wrote:

...

I'm interested in situations where you think fundeps work and type families don't.  Reason: no one knows how to make fundeps work cleanly with local type constraints (such as GADTs).

Simon,

I have run into a case where fundeps+MPTC seems to allow a more generalized instance declaration than type families.

The fundep+MPTC case:

{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances, UndecidableInstances #-}

class C a b c | a -> b, a -> c where    op :: a -> b -> c

instance C Bool a a where op _ = id

main = putStrLn $ op True "done"

In this case, I've (arbitrarily) chosen the Bool instance to be a no-op and pass through the types.  Because the dependent types are part of the declaration header I can use type variables for them.

That's really weird. In particular, I can add this line to your code without problems: foo = putStrLn $ if op True True then "done" else "." but GHC complains about this one: bar = putStrLn $ if op True True then op True "done" else "." fd.hs:14:0: Couldn't match expected type `Bool' against inferred type `[Char]' When using functional dependencies to combine C Bool [Char] String, arising from a use of `op' at fd.hs:14:38-51 C Bool Bool Bool, arising from a use of `op' at fd.hs:14:20-31 When generalising the type(s) for `bar' On the other hand, this is fine, but only with a type signature: baz :: a -> a baz = op True I don't think this is an intended feature of functional dependencies. -- Dave Menendez http://www.eyrie.org/~zednenem/

On Sat, 03 Jul 2010 12:48:56 -0700, Dan Doel wrote:

Then the instance declares infinitely many instances C Bool a a. This is a violation of the fundep. Based on your error message, it looks like it ends up treating the instance as the first concrete 'a' it comes across, but who knows?

Hmmm.. it doesn't look like a first concrete lockdown. The following works fine: opres1 :: Int -> Int opres1 = op True opres2 :: String -> String opres2 = op True main = do putStrLn $ op True "start" putStrLn $ show $ opres1 5 putStrLn $ opres2 $ opres2 $ show $ opres1 6 putStrLn $ opres2 "done" As a side note, although I agree it abuses the fundeps intent, it was handy for the specific purpose I was implementing to have a "no-op/passthrough" instance of op. In general I like the typedef approach better, but it looks like I must sacrifice the no-op to make that switch. -- -KQ

On Sat, 03 Jul 2010 13:28:44 -0700, Dan Doel wrote:

...

As a side note, although I agree it abuses the fundeps intent, it was handy for the specific purpose I was implementing to have a "no-op/passthrough" instance of op. In general I like the typedef approach better, but it

^^^^^^^ should have been "type family", not "typedef"

...

looks like I must sacrifice the no-op to make that switch. It's potentially not just a violation of intent, but of soundness.

I agree when examining this from the perspective of the compiler. It's an interesting little wormhole in the safety net usually provided by Haskell (or more properly GHC in this case) to stop people like me from doing foolish things. From the domain of the original problem, having a no-op instance is still desireable, and I achieved this by making the noop instance type polymorphic and use the target concrete type to guide the resolution of the interior family types. class C a where type A2 a type A3 a op :: a -> A2 a -> A3 a data NoOp x = NoOp instance C (NoOp b) where type A2 (NoOp x) = x type A3 (NoOp x) = x op _ = id This is straightforward and less ambiguous and should therefore be safer as well. Thanks and regards, -- -KQ