[Haskell-cafe] Equality constraints in type families
Claus Reinke
claus.reinke at talk21.com
Wed Mar 19 13:23:59 EDT 2008
>>> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
More information about the Haskell-Cafe
mailing list