[Haskell-cafe] Equality constraints in type families

[Claus Reinke]

>>> 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