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