type family F a :: * -> * .. We made the design choice that type functions with a higher-kinded result type must be injective with respect to the additional paramters. I.e. in your case:
F x y ~ F u v <=> F x ~ F u /\ y ~ v
actually, i don't even understand the first part of that:-( why would F x and F u have to be the same functions? shouldn't it be sufficient for them to have the same result, when applied to y and v, respectively? consider: -------------------------------------- type family G1 a :: * -> * type instance G1 a = G3 type family G2 a :: * -> * type instance G2 a = G4 type family G3 a :: * type instance G3 Bool = Bool type instance G3 Char = Bool type family G4 a :: * type instance G4 Bool = Char type instance G4 Char = Bool h :: G1 a Bool ~ G2 a Char => G1 a Bool h = True -------------------------------------- for which GHCi, version 6.9.20080317 happily infers *Main> :t h h :: G1 a Bool *Main> h True even though G1 a ~ G3 ~/~ G4 ~ G2 a ? claus
i'm still trying to understand this remark:
- if we are talking about "type functions", i should be allowed to replace a function application with its result, and if that result doesn't mention some parameters, they shouldn't play a role at any stage, right?
- if anything other than the function result matters, isn't it somewhat misleading to speak of "type functions"?
- if the parameters have to match irrespective of whether they appear in the result, that sounds like phantom types.
ok, but we're talking about a system that mixes unification with rewriting, so shouldn't the phantom parameters be represented in all rewrite results, just to make sure they cannot be ignored in any contexts?
ie, with
type instance F a = <rhs>
F a x should rewrite not to <rhs>, but to <rhs>_x, which would take care of the injectivity you want in the ~-case, but would also preserve the distinction if rewriting should come before ~, even if <rhs> managed to consume x, by being a constant function on types.
- things seem to be going wrong in the current implementation. consider this code, accepted by GHCi, version 6.9.20080317: ------------------------------------------ {-# 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) ------------------------------------------
(note the partially applied type synonym in the type instance, which is a constant function on types). it looks as if:
- False::Bool is accepted as Const Bool Bool - i::Const Bool Int is accepted as Bool - c::Const Bool Char is accepted as Bool - both i and c are accepted as Bool, so seem to be of an equivalent type, but aren't really.. - i::Const Bool Int is not accepted as Const Bool Char directly, but is accepted via one of the "eta expansions" for Bool, namely (&&True)
my current guess is that the implementation is incomplete, but that the idea of "type functions" also needs to be adjusted to take your design decision into account, with "phantom types" and type parameter annotations for type function results suggesting themselves as potentially helpful concepts?
or, perhaps, the implication isn't quite correct, and type parameters shouldn't be unified unless they appear in the result of applying the type function? the implementation would still be incomplete, but instead of rejecting more of the code, it should allow the commented-out case as well?
could you please help me to clear up this confusion?-)
thanks, claus
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe