Opened 6 years ago

Closed 6 years ago

Last modified 6 years ago

#2157 closed feature request (fixed)

Equality Constraints with Type Families

Reported by: hpacheco Owned by: chak
Priority: normal Milestone: 6.10 branch
Component: Compiler (Type checker) Version: 6.9
Keywords: Cc: hpacheco@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Difficulty: Unknown
Test Case: T2157 Blocked By:
Blocking: Related Tickets:

Description

For the implementation of fixpoint recursive definitions for a datatype I have defined the family:

type family F a :: * -> *
type FList a x = Either () (a,x)
type instance F [a] = FList a
type instance F Int = Either One

for which we can define functor instances

instance (Functor (F [a])) where
   fmap _ (Left _) = Left ()
   fmap f (Right (a,x)) = Right (a,f x)
...

However, in the definition of recursive patterns over these representation, I need some coercions to hold such as

F d c ~  F a (c,a)

but in the current implementation they are evaluated as

F d ~ F a /\ c ~(c,a)

what does not express the semantics of "fully parameterized equality" that I was expecting

You can find a pratical example in (my conversions at the haskell-cafe mailing list)

In order to avoid this, the family could be redefined as

type family F a x :: *
type instance F [a] x = Either() (a,x)
type instance F Int x = Either One x

but this would mean that I cannot define instances for Functor (F a) because not enough parameters passed to F.

PS. This might sound more as a feature request than a bug, so sorry if I misplaced this information. I am willing to work on this subject to help supporting my test case.

Change History (18)

comment:1 Changed 6 years ago by hpacheco

I meant conversations, not conversions :P

comment:2 follow-up: Changed 6 years ago by chak

  • Architecture changed from Unknown to Multiple
  • Component changed from Compiler to Compiler (Type checker)
  • Operating System changed from Unknown to Multiple
  • Owner set to chak
  • Type changed from bug to feature request

I'd like to find a solution here, but as far as I can see, there is no bug in GHC's type checker. In fact, if GHC would admit any of your code, it would also allow programs that are not type safe.

In particular, given your second definition,

type family F a x :: *

if we would allow partial applications, as in Functor (F a), we would get an inconsistent system; see Section 3.6 in http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html.

On the other hand, given

type family F a :: * -> *

an equality of the form F a1 b1 ~ F a2 b2 implies F a1 ~ F a2 and b1 ~ b2 as always in Haskell (this is what Mark Jones called higher-kinded unification in his paper about constructor classes).

In other words, given a type (f :: * -> * -> *), the partial application f t is well-formed exactly if the decomposition rule holds (i.e., f a1 b1 ~ f a2 b2 implies f a1 ~ f a2 and b1 ~ b2). These two properties are causally linked, you cannot get one without the other.

comment:3 in reply to: ↑ 2 ; follow-ups: Changed 6 years ago by claus

Replying to chak:

On the other hand, given

type family F a :: * -> *

an equality of the form F a1 b1 ~ F a2 b2 implies F a1 ~ F a2 and b1 ~ b2 as always in Haskell

i had problems with this statement, until i stopped thinking of "type functions" (which would allow constant functions violating your assumption) and thought of "phantom types" (all type parameters matter, even if they disappear in the result). if that association is useful, though, you might want to disallow partially applied type synonyms in type instances - Const and f seem fishy here (wrt your implication, at least):

{-# LANGUAGE TypeFamilies #-}

type family Const a :: * -> *
type instance Const a = C a
type C a t = a

f :: Const Bool Int -> Const Bool Char -> Const Bool Bool
f i c = False
-- f i c = i
-- f i c = i && True
-- f i c = (i || c) 

type family Const2 a :: * -> *
type instance Const2 a = Ct a
newtype Ct a t = Ct a

g :: Const2 Bool Int -> Const2 Bool Char -> Const2 Bool Bool
g i c = Ct False
-- g i c = Ct i
-- g i c = Ct (i && True)
-- g i c = Ct (i || c) 

for Const and f, GHCi, version 6.9.20080217 happily accepts i && True and i || c, converting between Const Bool * and Bool, but does not accept i.

comment:4 in reply to: ↑ 3 Changed 6 years ago by hpacheco

I understood your points and they do make sense, but do you think that this is a feasible feature request or it should never be supported?

I have just remembered that, still for the family

type family F a x :: *

type instance F [a] x = Either () (a,x)
type instance F Int x = Either () x

we can write "partial-evaluated classes for F" whenever not all type parameters are in use.
For the Functor class this would mean:

class FunctorF x where
	fmapF :: (a -> b) -> F x a -> F x b
	
instance FunctorF [a] where
   fmapF _ (Left _) = Left ()
   fmapF f (Right (a,x)) = Right (a,f x)

instance FunctorF Int where
   fmapF _ (Left ()) = Left ()
   fmapF f (Right n) = Right (f n)

At first glance it is less generic but seems to work.
However, a previous function (for the family F a :: * -> *)

hylo :: (Functor (F d)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
hylo d g h = g . fmap (hylo d g h) . h

if translated to

hylo :: (FunctorF d) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
hylo d g h = g . fmapF (hylo d g h) . h

does not compile with the explicit type signature.
Without a type signature it compiles and infers the signature (does not make sense to me)

hylo :: forall t d c a. (FunctorF d) => t -> (F d c -> c) -> (a -> F d a) -> a -> c

However, if this signature is passed explicitly, it does not compile again.
There must be a bug somewhere in this scheme, or am I missing something huge?

Regards,
hugo

comment:5 Changed 6 years ago by hpacheco

Well, it seems to work if the add a "magic" dummy argument to fmapF.

class FunctorF x where
	fmapF :: d -> (a -> b) -> F x a -> F x b

hylo :: (FunctorF d) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
hylo d g h = g . fmapF d (hylo d g h) . h

comment:6 follow-up: Changed 6 years ago by hpacheco

Curiously if I have

fff a = fmapF a id

it compiles correctly.
But if I infer the type signature of fff I get

fff :: forall d x. (FunctorF d) => d -> F d x -> F d x

On the other side, a similar problem as before arises when

fff :: forall d x. (FunctorF d) => d -> F d x -> F d x
fff a = fmapF a id

fails to compile.
This must be a bug. Sorry for all this posts.

comment:7 in reply to: ↑ 3 ; follow-up: Changed 6 years ago by chak

Replying to claus:

Replying to chak:

On the other hand, given

type family F a :: * -> *

an equality of the form F a1 b1 ~ F a2 b2 implies F a1 ~ F a2 and b1 ~ b2 as always in Haskell

i had problems with this statement, until i stopped thinking of "type functions" (which would allow constant functions violating your assumption) and thought of "phantom types" (all type parameters matter, even if they disappear in the result). if that association is useful, though, you might want to disallow partially applied type synonyms in type instances - Const and f seem fishy here (wrt your implication, at least):

{-# LANGUAGE TypeFamilies #-}

type family Const a :: * -> *
type instance Const a = C a
type C a t = a

Why do you think Const is fishy? Maybe I should make more precise what I regard as partial application in the context of type families. If you look at the type family specification in Section 7.1, it says that the arity of a type family is the number of parameters given in the type family declaration. In the case of Const, this is 1 (namely a), not 2 (as you might think if you only consider the kind of Const). Whenever a type family is used, you must supply at least as many type arguments as the arity of the type family suggests. So, in the case of Const, a single argument suffices. Do you think Section 7 of the type family specification is unclear on that matter. If so, I'd be grateful for any suggestions that make the specification clearer.

NB: The rules for what constitutes a valid partial application of a vanilla type synonym are different, see http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#type-synonyms This may be somewhat confusing, but I don't think there is much we can do about this, as the present definitions are crucial to get a sound type system. (Well, we could restrict what you can do with vanilla synonyms, but we'd like to stay backwards compatible to H98 and, I guess, people would also not be happy to sacrifice any of the currently offered expressiveness.)

comment:8 in reply to: ↑ 6 Changed 6 years ago by chak

Replying to hpacheco:

Curiously if I have

fff a = fmapF a id

it compiles correctly.
But if I infer the type signature of fff I get

fff :: forall d x. (FunctorF d) => d -> F d x -> F d x

On the other side, a similar problem as before arises when

fff :: forall d x. (FunctorF d) => d -> F d x -> F d x
fff a = fmapF a id

fails to compile.
This must be a bug. Sorry for all this posts.

No, it's not as bug. The problem is that the variable x occurs only as a type-index to the type family in the signature. Remember from above, as the arity of F is 2, given F a1 b1 ~ F a2 b2 we can not deduce that a1 ~ a2 and b1 ~ b2. (We need to explain that better in the type family documentation...)

comment:9 in reply to: ↑ 7 ; follow-up: Changed 6 years ago by claus

Replying to chak:

type family F a :: * -> *

an equality of the form F a1 b1 ~ F a2 b2 implies F a1 ~ F a2 and b1 ~ b2 as always in Haskell

i had problems with this statement, until i stopped thinking of "type functions" (which would allow constant functions violating your assumption) and thought of "phantom types" (all type parameters matter, even if they disappear in the result). if that association is useful, though, you might want to disallow partially applied type synonyms in type instances - Const and f seem fishy here (wrt your implication, at least):

{-# LANGUAGE TypeFamilies #-}

type family Const a :: * -> *
type instance Const a = C a
type C a t = a

Why do you think Const is fishy?

because:

  • type synonym C appears partially applied in what amounts to a type class instance parameter position (the rhs of the Const instance)
  • the implementation definitely does not behave as if your decomposition played any role (parameters of both Const Bool Int and Const Bool Char are used as/converted to Bool, hence equal types even though Int does not equal Char). nor do the permitted and not-permitted conversions in f seem consistent - compare also:

http://www.haskell.org/pipermail/haskell-cafe/2008-March/040788.html

http://www.haskell.org/pipermail/haskell-cafe/2008-March/040790.html

Maybe I should make more precise what I regard as partial application in the context of type families.

it isn't about partial applications of type families (even though the different sorts of parameters there take some getting used to), but about good old-fashioned partial applications of type synonyms in new contexts. i guess they are permitted here because the rhs of a type instance uses the same grammar non-terminal as the rhs of a type synonym, but i suspect that the rhs of a type instance might have to be treated like a type parameter of a type class instance.

but that is just a guess - the main issues here are the decomposition rule, which i don't quite understand, and which doesn't quite seem to be used in the implementation, and the equalities/conversions permitted in the implementation, which do not seem to be consistent.

comment:1 in reply to: ↑ 9 Changed 6 years ago by chak

Replying to claus:

Replying to chak:

{-# LANGUAGE TypeFamilies #-}

type family Const a :: * -> *
type instance Const a = C a
type C a t = a

Why do you think Const is fishy?

because:

  • type synonym C appears partially applied in what amounts to a type class instance parameter position (the rhs of the Const instance)

I don't agree that the lhs of a type instance amounts to a type class instance parameter position; type instance have nothing to do with type classes.

However, I think I now understand what you are worried about. It is the interaction of type families and GHC's generalised type synonyms (i.e., type synonyms that may be partially applied). I agree that it does lead to an odd interaction, because the outcome may depend on the order in which the type checker performs various operations. In particular, whether it first applies a type instance declaration to reduce a type family application or whether it first performs decomposition.

The most clean solution may indeed be to outlaw partial applications of vanilla type synonyms in the rhes of type instances. (Which is what I will implement unless anybody has a better idea.)

comment:13 Changed 6 years ago by igloo

  • Difficulty set to Unknown
  • Milestone set to 6.10 branch

comment:14 Changed 6 years ago by hpacheco

  • Cc hpacheco@… added

comment:15 Changed 6 years ago by chak

  • Resolution set to fixed
  • Status changed from new to closed

I fixed the checking of rhss of type family instances. Otherwise, I don't think there is anything that we can do about this; hence, I close the ticket.

comment:16 Changed 6 years ago by chak

  • Test Case set to T2157

comment:17 Changed 6 years ago by simonmar

  • Architecture changed from Multiple to Unknown/Multiple

comment:18 Changed 6 years ago by simonmar

  • Operating System changed from Multiple to Unknown/Multiple
Note: See TracTickets for help on using tickets.