Equality constraints in type families

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
47 messages Options
123
Reply | Threaded
Open this post in threaded view
|

Equality constraints in type families

Hugo Pacheco
Hi all,

I have encoded a type family such that:

type family F a :: * -> *

and a function (I know it is complicated, but I think the problem is self explanatory):

hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a (c,a)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
hyloPara d g h = g . fmap (hyloPara d g h) . h

it all works fine.

However, if I change the declaration to (changed F d c for the "supposedly equivalent" F a (c,a)):

hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a (c,a)) => d -> (F a (c,a) -> c) -> (a -> F d a) -> a -> c

and I get

    Occurs check: cannot construct the infinite type: c = (c, a)
    When generalising the type(s) for `hyloPara'

This really messes up my notions on equality constraints, is it the expected behavior? It would be essential for me to provide this definition.

Thanks,
hugo


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Tom Schrijvers-2

Hi Hugo,

> I have encoded a type family such that:
>
> type family F a :: * -> *
>
> and a function (I know it is complicated, but I think the problem is self
> explanatory):
>
> hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a
> (c,a)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c
> hyloPara d g h = g . fmap (hyloPara d g h) . h
>
> it all works fine.
>
> However, if I change the declaration to (changed F d c for the
> "supposedly equivalent" F a (c,a)):
>
> hyloPara :: (Functor (F a), Functor (F d), F d a ~ F a (a,a), F d c ~ F a
> (c,a)) => d -> (F a (c,a) -> c) -> (a -> F d a) -> a -> c
>
> and I get
>
>    Occurs check: cannot construct the infinite type: c = (c, a)
>    When generalising the type(s) for `hyloPara'
>
> This really messes up my notions on equality constraints, is it the expected
> behavior? It would be essential for me to provide this definition.

I think you've uncovered a bug in the type checker. 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

So if we apply that to F d c ~ F a (c,a) we get:

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

where the latter clearly is an occurs-check error, i.e. there's no finite
type c such that c = (c,a). So the error in the second version is
justified. There should have been one in the latter, but the type checker
failed to do the decomposition: a bug.

What instances do you have for F? Are they such that F d c ~ F a (c,a) can
hold?

By the way, for your function, you don't need equations in your type
signature. This will do:

  hyloPara ::
  Functor (F d)
  => d
  -> (F d c -> c)
  -> (a -> F d a)
  -> a
  -> c

Cheers,

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Hugo Pacheco
I know I do not need these constraints, it was just the simplest way I found to explain the problem.

I have fought about that: I was not expecting F d c ~  F a (c,a) not mean that F d ~F a /\ c ~(c,a), I thought the whole family was "parameterized".
If I encoded the family

type family F a x :: *

F d c ~  F a (c,a) would be semantically different, meaning that this "decomposition rule" does not apply?

Thanks,
hugo






_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Tom Schrijvers-2
On Tue, 11 Mar 2008, Hugo Pacheco wrote:

> I know I do not need these constraints, it was just the simplest way I found
> to explain the problem.
>
> I have fought about that: I was not expecting F d c ~  F a (c,a) not mean
> that F d ~F a /\ c ~(c,a), I thought the whole family was "parameterized".
> If I encoded the family
>
> type family F a x :: *
>
> F d c ~  F a (c,a) would be semantically different, meaning that this
> "decomposition rule" does not apply?

Correct. However, then you cannot write "Functor (F a)" because
type functions must be fully applied. So either way you have a problem.

Could you show the type instances for F you have (in mind)? This way we
can maybe see whether what you want to is valid and the type checker could
be adjusted to cope with it, or whether what you're trying to do would
not be valid (in general).

I have my suspicions about your mentioning of both Functor (F d) and
Functor (F a) in the signature. Which implementation of fmap do you want?
Or should they be both the same (i.e. F d ~ F a)?

Cheers,

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Hugo Pacheco
Yes, I have tried both implementations at the start and solved it by choosing for the following:

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

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

The option was:

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

instance (Functor (F [a])) where -- error, not enough parameters passed to F
fmap _ (Left _) = Left ()
fmap f (Right (a,x)) = Right (a,f x)

So, indeed, with either implementation I have a problem.

>I have my suspicions about your mentioning of both Functor (F d) and
>Functor (F a) in the signature. Which implementation of fmap do you want?
>Or should they be both the same (i.e. F d ~ F a)?


This is an hard question to which the answer is both.

In the definition of an hylomorphism I want the fmap from (F d):

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

However, those constraints I have asked about would allow me to encode a paramorphism as an hylomorphism:

class Mu a where
    inn :: F a a -> a
    out :: a -> F a a

para :: (Mu a, Functor (F a),Mu d, Functor (F d),F d a ~ F a (a,a), F d c ~ F a (c,a)) => d -> (F a (c,a) -> c) -> a -> c
para d f = hylo d f (fmap (id /\ id) . out)

In para, I would want the fmap from (F a) but that would be implicitly forced by the usage of out :: a -> F a a

Sorry for all the details, ignore them if they are too confusing.
Do you think there might be a definition that would satisfy me both Functor instances and equality?

Thanks for your pacience,
hugo

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Tom Schrijvers-2
On Tue, 11 Mar 2008, Hugo Pacheco wrote:

> Yes, I have tried both implementations at the start and solved it by
> choosing for the following:
> type family F a :: * -> *
> type FList a x = Either () (a,x)
> type instance F [a] = FList a
>
> instance (Functor (F [a])) where
> fmap _ (Left _) = Left ()
> fmap f (Right (a,x)) = Right (a,f x)

For this implementation we do have that

  F [a] b ~ F [c] d

  <=>

  F [a] ~ F [c] /\ b ~ d

Right? So for this instance, your para via hylo wouldn't work anyway.

I'd like to see some type instances and types such that the equation F d a
~ F a (a,a) holds. With your example above, it's not possible to make the
equation hold, .e.g.

F [t] [s]         ~ F [s] ([s],[s])
<=>
Either () (t,[s]) ~ Either ()(s,([s],[s]))

is not true for any (finite) types t and s.

Do you have such an example? You should have one, if you want to be able to call para.

Tom

>> I have my suspicions about your mentioning of both Functor (F d) and
>> Functor (F a) in the signature. Which implementation of fmap do you want?
>> Or should they be both the same (i.e. F d ~ F a)?
>
> This is an hard question to which the answer is both.
>
> In the definition of an hylomorphism I want the fmap from (F d):
>
> 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
>
> However, those constraints I have asked about would allow me to encode a
> paramorphism as an hylomorphism:
>
> class Mu a where
>    inn :: F a a -> a
>    out :: a -> F a a
>
> para :: (Mu a, Functor (F a),Mu d, Functor (F d),F d a ~ F a (a,a), F d c ~
> F a (c,a)) => d -> (F a (c,a) -> c) -> a -> c
> para d f = hylo d f (fmap (id /\ id) . out)
>
> In para, I would want the fmap from (F a) but that would be implicitly
> forced by the usage of out :: a -> F a a
>
> Sorry for all the details, ignore them if they are too confusing.
> Do you think there might be a definition that would satisfy me both Functor
> instances and equality?
>
> Thanks for your pacience,
> hugo
>

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Hugo Pacheco
That's simple Tom.
Imagine the factorial function for Int written as a paramorphism:

type instance F Int = Either One

instance (Mu Int) where
    inn (Left _) = 0
    inn (Right n) = succ n
    out 0 = Left ()
    out n = Right (pred n)

instance Functor (F Int) where
    fmap _ (Left ()) = Left ()
    fmap f (Right n) = Right (f n)

fact :: Int -> Int
fact = para (const 1 \/ (uncurry (*)) . (id >< succ))

If we consider that the paramorphism is implemented as an hylomorphism, then an intermediate virtual type (d in the hylo definition) [Int]

If you test the constraints for d = [Int], a = Int and c = Int

F d c ~ F a (c,a)

F d a = F [Int] Int = Either One (Int,Int)
F a (c,a) = F Int (Int,Int) = Either One (Int,Int)

F d a ~ F a (a,a)

F d a = F a (a,a) -- pure substitution of the above case

Hope this helps.
Thanks again for you patience,
hugo



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Claus Reinke
In reply to this post by Tom Schrijvers-2
>> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Tom Schrijvers-2
> could you please help me to clear up this confusion?-)

Let me summarize :-)

The current design for type functions with result kinds other than *
(e.g. * -> *) has not gotten very far yet. We are currently stabilizing
the ordinary * type functions, and writing the story up. When that's done
we can properly focus on this issue and consider different design choices.

Cheers,

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Claus Reinke
In reply to this post by 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Claus Reinke
In reply to this post by Tom Schrijvers-2
> Let me summarize :-)
>
> The current design for type functions with result kinds other than *
> (e.g. * -> *) has not gotten very far yet. We are currently stabilizing
> the ordinary * type functions, and writing the story up. When that's done
> we can properly focus on this issue and consider different design choices.

thanks, seems i was too optimistic, then!-)

btw, i noticed that the user guide points to the haskell wiki only,
while the latest info seems to be on the ghc wiki. given the number
of variations and the scope of development, it would also be
helpful if the user guide had at least a one-paragraph executive
summary of the state of play, dated to clarify how up-to-date
that summary is.

that would avoid discussions of not yet stabilized features
(should ghc issue a warning when such are used?).

claus


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Manuel M T Chakravarty
In reply to this post by Claus Reinke
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
>
> 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"?

You will notice that I avoid calling them "type functions".  In fact,  
the official term is "type families".  That is what they are called in  
the spec <http://haskell.org/haskellwiki/GHC/Type_families> and GHC's  
option is -XTypeFamilies, too.  More precisely, they are "type-indexed  
type families".

One difference between type families and (value-level) functions is  
that not all parameters of a type family are treated the same.  A type  
family has a fixed number of type indicies.  We call the number of  
type indicies the type family's arity and by convention, the type  
indicies come always before other type parameters.  In the example

   type family F a :: * -> *

F has arity 1, whereas

   type family G a b :: *

has arity 2.  So, the number of named parameters given is the arity.  
(The overall kind is still F :: * -> * -> *; ie, the arity is not  
obvious from the kind, which I am somewhat unhappy about.)  In other  
words, in a type term like (F Int Bool), the two parameters Int and  
Bool are treated differently.  Int is treated like a parameter to a  
function (which is what you where expecting), whereas Bool is treated  
like a parameter to a vanilla data constructor (the part you did not  
expect).  To highlight this distinction, we call only Int a type  
index.  Generally, if a type family F has arity n, it's first n  
parameters are type indicies, the rest are treated like the parameters  
of any other type constructor.  Moreover, a type family of arity n,  
must always be applied to at least n parameters - ie, applications to  
type indicies cannot be partial.

This is not just an arbitrary design decision, it is necessary to stay  
compatible with Haskell's existing notion of higher-kinded unification  
(see, Mark Jones' paper about constructor classes), while keeping the  
type system sound.  To see why, consider that Haskell's higher-kinded  
type system, allows type terms, such as (c a), here c may be  
instantiated to be (F Int) or Maybe.  This is only sound if F treats  
parameters beyond its arity like any other type constructor.  A more  
formal discussion is in our TLDI paper about System F_C(X).

Manuel

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Manuel M T Chakravarty
In reply to this post by Tom Schrijvers-2
Tom Schrijvers:
>> could you please help me to clear up this confusion?-)
>
> Let me summarize :-)
>
> The current design for type functions with result kinds other than *
> (e.g. * -> *) has not gotten very far yet. We are currently  
> stabilizing the ordinary * type functions, and writing the story up.  
> When that's done we can properly focus on this issue and consider  
> different design choices.

I don't quite agree.  The current story was pretty much settled in the  
paper on associated type synonyms already and further clarified in the  
FC paper.

Manuel

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Manuel M T Chakravarty
In reply to this post by Claus Reinke
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?

Oh, yes, that is sufficient and exactly what is meant by F x ~ F u.  
It means, the two can be unified modulo any type instances and local  
given equalities.

Manuel

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Claus Reinke
In reply to this post by Manuel M T Chakravarty
>>>> type family F a :: * -> *
>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v
>>
> words, in a type term like (F Int Bool), the two parameters Int and  
> Bool are treated differently.  Int is treated like a parameter to a  
> function (which is what you where expecting), whereas Bool is treated  
> like a parameter to a vanilla data constructor (the part you did not  
> expect).  To highlight this distinction, we call only Int a type  
> index.  Generally, if a type family F has arity n, it's first n  
> parameters are type indicies, the rest are treated like the parameters  
> of any other type constructor.  

i'm not sure haskell offers the kind of distinction that we
need to talk about this: 'data constructor' is value-level,
'type constructor' doesn't distinguish between type- vs
data-defined type constructors. i think i know what you
mean, but it confuses me that you use 'data constructor'
(should be data/newtype-defined type constructor?)
and 'type constructor' (don't you want to exclude
type-defined type constructors here).

    data ConstD x y = ConstD x
    type ConstT x y = x

'ConstD x' and 'ConstT x' have the same kind, that
of type constructors: * -> *. but:

    ConstD x y1 ~ ConstD x y2 => y1 ~ y2

whereas

    forall y1, y2: ConstT x y1 ~ ConstT x y2

and i thought 'type family' was meant to suggest type
synonym families, in contrast to 'data family'?

you did notice that i gave an example of how ghc does
not seem to follow that decomposition rule, didn't you?
ghc seems to behave almost as i would expect, not as
the decomposition rule seems to suggest.

still confused,
claus


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Claus Reinke
In reply to this post by Manuel M T Chakravarty
>>>>> type family F a :: * -> *
>>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v
>>
>> 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?
>
> Oh, yes, that is sufficient and exactly what is meant by F x ~ F u.  
> It means, the two can be unified modulo any type instances and local  
> given equalities.

sorry, i don't understand how that could be meant by 'F x ~ F u';
that equality doesn't even refer to any specific point on which these
two need to be equal, so it can only be a point-free higher-order
equality, can't it?

the right-to-left implication is obvious, but the left-to-right
implication seems to say that, for 'F x' and 'F u' to be equal on
any concrete pair of types 'y' and 'u', they have to be equal on
all possible types and 'y' and 'u' themselves have to be equal.

again, i gave a concrete example of how ghc behaves as i
would expect, not as that decomposition rule would suggest.

i'll try to re-read the other paper you suggested, but it would
help me if you could discuss the two concrete examples i
gave in this thread.

thanks,
claus


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Manuel M T Chakravarty
In reply to this post by Claus Reinke
Claus Reinke:

>>>>> type family F a :: * -> *
>>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v
>>>
>> words, in a type term like (F Int Bool), the two parameters Int  
>> and  Bool are treated differently.  Int is treated like a parameter  
>> to a  function (which is what you where expecting), whereas Bool is  
>> treated  like a parameter to a vanilla data constructor (the part  
>> you did not  expect).  To highlight this distinction, we call only  
>> Int a type  index.  Generally, if a type family F has arity n, it's  
>> first n  parameters are type indicies, the rest are treated like  
>> the parameters  of any other type constructor.
>
> i'm not sure haskell offers the kind of distinction that we
> need to talk about this: 'data constructor' is value-level,
> 'type constructor' doesn't distinguish between type- vs
> data-defined type constructors. i think i know what you
> mean, but it confuses me that you use 'data constructor'
> (should be data/newtype-defined type constructor?)

Yes, I meant to write "data type constructor".

> and 'type constructor' (don't you want to exclude
> type-defined type constructors here).

It may have been clearer if I had written data type constructor, but  
then the Haskell 98 report doesn't bother with that either (so I tend  
to be slack about it, too).

>   data ConstD x y = ConstD x
>   type ConstT x y = x
>
> 'ConstD x' and 'ConstT x' have the same kind, that
> of type constructors: * -> *. but:
>
>   ConstD x y1 ~ ConstD x y2 => y1 ~ y2
>
> whereas
>
>   forall y1, y2: ConstT x y1 ~ ConstT x y2

But note that

   ConstT x ~ ConstT x

is malformed.

> and i thought 'type family' was meant to suggest type
> synonym families, in contrast to 'data family'?

My nomenclature is as follows.  The keywords 'type family' introduces  
a "type synonym family" and 'data family' introduces a "data type  
family" (or just "data family").  The term "type family" includes  
both.  This follows Haskell's common use of "type constructor", "type  
synonym constructor", and "data type constructor".

> you did notice that i gave an example of how ghc does
> not seem to follow that decomposition rule, didn't you?

Yes, but I didn't see why you think GHC does the wrong thing.

Manuel
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Manuel M T Chakravarty
In reply to this post by Claus Reinke
Claus Reinke:

>>>>>> type family F a :: * -> *
>>>>> F x y ~ F u v <=> F x ~ F u /\ y ~ v
>>>
>>> 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?
>> Oh, yes, that is sufficient and exactly what is meant by F x ~ F  
>> u.   It means, the two can be unified modulo any type instances and  
>> local  given equalities.
>
> sorry, i don't understand how that could be meant by 'F x ~ F u';
> that equality doesn't even refer to any specific point on which these
> two need to be equal, so it can only be a point-free higher-order
> equality, can't it?
>
> the right-to-left implication is obvious, but the left-to-right
> implication seems to say that, for 'F x' and 'F u' to be equal on  
> any concrete pair of types 'y' and 'u', they have to be equal on all  
> possible types and 'y' and 'u' themselves have to be equal.

You write 'y' and 'u'.  Do you mean 'x' and 'u'?  If so, why do you  
think the implication indicates that x and u need to be the same?

> again, i gave a concrete example of how ghc behaves as i would  
> expect, not as that decomposition rule would suggest.

Maybe you can explain why you think so.  I didn't understand why you  
think the example is not following the decomposition rule.

Manuel

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Manuel M T Chakravarty
Manuel M T Chakravarty:
>> again, i gave a concrete example of how ghc behaves as i would  
>> expect, not as that decomposition rule would suggest.
>
> Maybe you can explain why you think so.  I didn't understand why you  
> think the example is not following the decomposition rule.

Actually, see

   http://hackage.haskell.org/trac/ghc/ticket/2157#comment:10

Manuel

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Equality constraints in type families

Claus Reinke
>>> again, i gave a concrete example of how ghc behaves as i would  
>>> expect, not as that decomposition rule would suggest.
>>
>> Maybe you can explain why you think so.  I didn't understand why you  
>> think the example is not following the decomposition rule.
>
> Actually, see
>
>   http://hackage.haskell.org/trac/ghc/ticket/2157#comment:10
>
> Manuel

for those following along here:

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

yes, indeed, thanks! that was the central point of example one.

one might say that the central point of example two were two
partially applied type synonym families in the same position
(rhs of a type synonym family instance definition).

usually, when reduction meets typing, there is a subject reduction
theorem, stating that types do not change during reduction. since,
in this case, reduction and constraint generation happen at the
same (type) level, the equivalent would be a proof of confluence,
so that it doesn't matter which type rules are applied in which
order (in this case, decomposition and reduction).

as far as i could determine, the TLDI paper does not deal with
the full generality of ghc's type extensions, so it doesn't stumble
over this issue, and might need elaboration.

my suggestion was to annotate the results of type family application
reductions with the type parameters. in essence, that would carry
the phantom types along for type checking, and the decomposition
rule could be taken care of even after reduction, by comparing these
annotations. alternatively, use the decomposition rule as the reduction
rule. both would make clear that one is *not* dealing with simple
type-level function applications.

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

i always dislike losing expressiveness, and ghc does almost seem
to behave as i would expect in those examples, so perhaps there
is a way to fit the partial applications into the theory of your TLDI
paper. and i still don't like the decomposition rule, and i still don't
even understand that first part about comparing partially applied
type constructors!-)

but in terms of actually implementing your design, and matching
your theory and proofs, it might be best to treat the rhs of a type
family instance like a type class instance parameter (where partial
applications of synonyms and families are ruled out), not like the
rhs of a type synonym definition (where everything is allowed).

then users can try out an implementation that does what you
say it would, including constraints needed for your proofs, which
might lead to extension requests later - as Tom said, there may
still be some open ends. perhaps you could keep those two
examples around in a separate ticket, collecting experiences
with and limitations of type families?

thanks,
claus


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
123