[Haskell-cafe] 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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Tom Schrijvers]

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: [EMAIL PROTECTED]
url: http://www.cs.kuleuven.be/~toms/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] 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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Tom Schrijvers]

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: [EMAIL PROTECTED]
url: http://www.cs.kuleuven.be/~toms/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] 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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Tom Schrijvers]

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: [EMAIL PROTECTED]
url: http://www.cs.kuleuven.be/~toms/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] 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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [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


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 = 

   F a x should rewrite not to , but to _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  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

Re: [Haskell-cafe] Equality constraints in type families

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


Cheers,

Tom

--
Tom Schrijvers

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

tel: +32 16 327544
e-mail: [EMAIL PROTECTED]
url: http://www.cs.kuleuven.be/~toms/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [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 = 

   F a x should rewrite not to , but to _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  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

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Claus Reinke]

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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

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  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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[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?)
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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

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


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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] 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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] 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
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

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


oops, sorry, i meant 'y' and 'v' - the second parameters.

but my concern here was with the 'F x ~ F u' part - since
it doesn't refer to the 'y' and 'v' parameters, i suspect that 
means a semantic comparison over all possible parameters


   forall y,v: F x y ~ F u v

ie, comparing the type-level 'functions', implying some decidable
approximation. my second example, using two partially applied 
type families G3 and G4, aimed to demonstrate that this doesn't 
happen in ghc, and that equality on specific points is sufficient. 


perhaps you want to exclude those partial applications as well,
but i'm concerned that type families appear less and less as
the straightforward type-level functional programming that i
was hoping for. in fact, the decomposition rule seems to be 
saying that type function results cannot matter, only the 
structure of type family applications does:


   F x y ~ F u v <=> F x ~ F u /\ y ~ v

or do you have a specific type rule application order in mind
where all type-level reductions are performed before this
decomposition rule can be applied?

claus


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Claus Reinke]

was hoping for. in fact, the decomposition rule seems to be 
saying that type function results cannot matter, only the 
structure of type family applications does:


   F x y ~ F u v <=> F x ~ F u /\ y ~ v

or do you have a specific type rule application order in mind
where all type-level reductions are performed before this
decomposition rule can be applied?


hmm, it seems that here i was confused by the extra syntactic
restrictions you have alluded to, meaning that the decomposition
rule only applies to extra parameters, not to the type indices.
also, given

   type family F a :: * -> *

'F x' and 'F u' are full applications, so may still be rewritten
according to the family instance rules, which means that
decomposition does not prevent reduction.

it would really be helpful to have local indications of such
differences that have an influence on interpretation, eg, a
way to distinguish the type indices from the extra parameters.

given that type families are never meant to be partially 
applied, perhaps a different notation, avoiding confusion

with type constructor applications in favour of something
resembling products, could make that clearer?

something simple, like braces to group families and indices:

   type family {F a} :: * -> *
   {F x} y ~ {F u} v <=> {F x} ~ {F u} && y ~ v

would avoid confusion about which parameters need
to be present (no partial application possible) and are
subject to family instance rules, and which parameters 
are subject to the decomposition rule.


assuming that you are going to rule out partial applications
of type synonyms (example 1) and type families (example 2)
in the rhs of type family instances for now, i think that answers
my questions in this thread, although i'd strongly recommend
the alternative syntax, grouping type indices with braces.

sorry about the confusion,
claus


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

RE: [Haskell-cafe] Equality constraints in type families

[Simon Peyton-Jones]

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

Aha.

Just to clarify, then, GHC's 'generalised type synonyms' behave like this.

* H98 says that programmer-written types must obey certain constraints:
- type synonym applications saturated
- arguments of type applications are monotypes (apart from ->)

* GHC says that these constraints must be obeyed only
*after* the programmer-written type has been normalised
by expanding saturated type synonyms

http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#type-synonyms

I regard this as a kind of pre-pass, before serious type checking takes place, 
so I don't think it should interact with type checking at all.

I don't think this normalisation should include type families, although H98 
type synonyms are a kind of degenerate case of type families.

Would that design resolve this particular issue?

Simon

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Dan Doel]

On Tuesday 11 March 2008, Tom Schrijvers wrote:
> 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.

While I think I understand why this is (due to the difference between index 
and non-index types), does this mean the following won't type check (it does 
in 6.8, but I gather its type family implementation wasn't exactly complete)?

type family D a :: *
type family E a :: *

type instance D Int  = Char
type instance D Char = Int

type instance E Char = Char
type instance E Int  = Int

type family F a :: * -> *

type instance F Int  = D
type instance F Char = E

foo :: F Int Int ~ F Char Char => a
foo = undefined

Clearly, both F Int Int ~ Char and F Char Char ~ Char, but neither Int ~ Char 
nor F Int ~ F Char.

Then again, looking at that code, I guess it's an error to have D and E 
partially applied like that? And one can't write, say:

type instance F Int a = D a

correct? I suppose that clears up situations where one might be able to 
construct a specific F X Y ~ F U V, but F X /~ F U \/ Y /~ V (at least, I 
can't thing of any others off the top of my head).

Thanks.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[David Menendez]

On Mon, Mar 24, 2008 at 12:14 AM, Manuel M T Chakravarty
<[EMAIL PROTECTED]> wrote:
>  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.)

Perhaps type families could use a different kind constructor to
distinguish type indexes from type parameters.

Currently, Haskell kinds are generated by this grammar:

   kind ::= "*" | kind "->" kind

We create a new production for "family kinds",

   fkind ::= kind | kind "-|>" fkind

Now, we can easily distinguish F and G,

   F :: * -|> * -> *
   G :: * -|> * -|> *

The grammar allows higher-kinded indexes, like (* -> *) -|> *, but
requires all indexes to precede the regular parameters. (That is, you
can't abstract over a family.)

-- 
Dave Menendez <[EMAIL PROTECTED]>

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Simon Peyton-Jones:
| | 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.

Aha.

Just to clarify, then, GHC's 'generalised type synonyms' behave like  
this.


* H98 says that programmer-written types must obey certain  
constraints:

   - type synonym applications saturated
   - arguments of type applications are monotypes (apart from ->)

* GHC says that these constraints must be obeyed only
   *after* the programmer-written type has been normalised
   by expanding saturated type synonyms

http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#type-synonyms

I regard this as a kind of pre-pass, before serious type checking  
takes place, so I don't think it should interact with type checking  
at all.


I don't think this normalisation should include type families,  
although H98 type synonyms are a kind of degenerate case of type  
families.


Would that design resolve this particular issue?


Not quite, but it refines my proposal of requiring that type synonyms  
in the rhs of type instances need to be saturated.  Let me elaborate.


The current implementation is wrong, as it permits

  type S a b = a
  type family F a :: * -> *
  type instance F a = S a

Why do we need to forbid this type instance?  Because it breaks the  
confluence of equality constraint normalisation.  Here are two  
diverging normalisations:


  (1)

F Int Bool  ~  F Int Char

  ==> DECOMP

F Int ~ F Int, Bool ~ Char

  ==> FAIL


  (2)

F Int Bool  ~  F Int Char

  ==> TOP

S Int Bool  ~  S Int Char

  ==> (expand type synonym)

Int  ~  Int

  ==> TRIVIAL

However, here is a (somewhat silly) program that does have partially  
applied type synonyms in a type instances' rhs and that is perfectly ok:


  type S a b = a
  type family F (a :: * -> *) b :: * -> *
  type instance F a b = S (S a) b b

This is ok, because we can expand the type synonyms in the rhs of the  
type instance


  S (S a) b b = S a b = a

and get a valid type.

So, the crucial point is that, as you wrote,

I don't think this normalisation should include type families,  
although H98 type synonyms are a kind of degenerate case of type  
families.


The only way to stratify the normalisation of type synonyms and type  
families such that all type synonyms are expanded before any family  
applications are normalised is by requiring that after normalising the  
rhs of a type instance declaration *by itself*, we get a type that  
only contains saturated applications of type synonyms.  (As Claus  
wrote, this is after all what we do for class instance heads.)


Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Claus Reinke:

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


Well, we still need normal subject reduction (i.e., types don't change  
under value term reduction), and we have established that for System  
FC (in the TLDI paper).


In addition, type term normalisation (much like value term  
normalisation) needs to be confluent; otherwise, you won't get a  
complete type inference/checking algorithm.



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.


System FC as described in the paper is GHC's current Core language.   
What are you missing?


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


I don't think we can avoid losing that expressiveness, as you  
demonstrated that it leads to non-confluence of type term  
normalisation - see also my reply to SimonPJ's message in this thread.



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


Haskell always had the decomposition rule.  Maybe we confused the  
matter, by always showing a particular instance of the decomposition  
rule, rather than the general rule.  Here it is in all it's glory:


  t1 t2 ~ t1' t2'  <==>  t1 ~ t1', t2 ~ t2'

No mention of a type family.  However, the rule obviously still needs  
to be correct if we allow any of the type terms (including t1 and t1')  
to include *saturated* applications of type families.


Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Claus Reinke wrote,
given that type families are never meant to be partially applied,  
perhaps a different notation, avoiding confusion

with type constructor applications in favour of something
resembling products, could make that clearer?

something simple, like braces to group families and indices:

  type family {F a} :: * -> *
  {F x} y ~ {F u} v <=> {F x} ~ {F u} && y ~ v

would avoid confusion about which parameters need
to be present (no partial application possible) and are
subject to family instance rules, and which parameters are subject  
to the decomposition rule.



and David Menendez wrote,

erhaps type families could use a different kind constructor to
distinguish type indexes from type parameters.

Currently, Haskell kinds are generated by this grammar:

  kind ::= "*" | kind "->" kind

We create a new production for "family kinds",

  fkind ::= kind | kind "-|>" fkind

Now, we can easily distinguish F and G,

  F :: * -|> * -> *
  G :: * -|> * -|> *

The grammar allows higher-kinded indexes, like (* -> *) -|> *, but
requires all indexes to precede the regular parameters. (That is, you
can't abstract over a family.)


Yes, this is something that we thought about, too.  In the System FC  
paper, we subscript all type families with their arity to achieve a  
weak form of this; ie, we'd write


  F_1 Int Bool

to make clear that (F_1 Int) is a non-decomposable family application,  
where the outermost application in ((F_1 Int) Bool) is decomposable.


The extra syntax has its advantages (more local information) and  
disadvantages (more clutter).  We weren't convinced that we need the  
extra syntax, so left it out for the moment. However, this is  
something that can always be changed if experience shows that programs  
are easier to understand with extra syntax.  It doesn't affect the  
type theory and is really a pure language design question.  I'd be  
glad to hear some more opinions about this matter.


Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Hugo Pacheco]

> The extra syntax has its advantages (more local information) and
> disadvantages (more clutter).  We weren't convinced that we need the
> extra syntax, so left it out for the moment. However, this is
> something that can always be changed if experience shows that programs
> are easier to understand with extra syntax.  It doesn't affect the
> type theory and is really a pure language design question.  I'd be


I would go for the braces as Claus suggested, although not necessary they
would have helped me to better understand how type family application
behaves.

> | 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.
>
> I don't think we can avoid losing that expressiveness, as you
> demonstrated that it leads to non-confluence of type term
> normalisation - see also my reply to SimonPJ's message in this thread.
> glad to hear some more opinions about this matter.


Since I was the one to start this thread, I have managed to implement what I
initially wanted as F a :: *->* with F a x::*, and the cost of not having
partially applied type synonyms was not much apart from some more equality
coercions that I wasn't expecting.
The most relevant tradeoffs are some more extra parameters in type classes
(notice the d in fmapF) and having to bind explicit signatures to variables
that only occur as a type-index to the type family (notice id::x->x).

class FunctorF x where fmapF :: d -> (a -> b) -> F x a -> F x b
fff :: forall d x. (FunctorF d) => d -> F d x -> F d x
fff a = fmapF a (id::x->x)

Generally, I love type-indexed types.
hugo
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Dan Doel:

On Tuesday 11 March 2008, Tom Schrijvers wrote:
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.


While I think I understand why this is (due to the difference  
between index
and non-index types), does this mean the following won't type check  
(it does
in 6.8, but I gather its type family implementation wasn't exactly  
complete)?


   type family D a :: *
   type family E a :: *

   type instance D Int  = Char
   type instance D Char = Int

   type instance E Char = Char
   type instance E Int  = Int

   type family F a :: * -> *

   type instance F Int  = D
   type instance F Char = E

   foo :: F Int Int ~ F Char Char => a
   foo = undefined

Clearly, both F Int Int ~ Char and F Char Char ~ Char, but neither  
Int ~ Char

nor F Int ~ F Char.

Then again, looking at that code, I guess it's an error to have D  
and E

partially applied like that?


Exactly.


And one can't write, say:

   type instance F Int a = D a

correct? I suppose that clears up situations where one might be able  
to
construct a specific F X Y ~ F U V, but F X /~ F U \/ Y /~ V (at  
least, I

can't thing of any others off the top of my head).


Yes, this type instance is invalid.  However, early version of the  
type family implementation erroneously accepted such instances.


Manuel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

RE: [Haskell-cafe] Equality constraints in type families

[Simon Peyton-Jones]

| > * GHC says that these constraints must be obeyed only
| >*after* the programmer-written type has been normalised
| >by expanding saturated type synonyms
| >
...
| > I regard this as a kind of pre-pass, before serious type checking
| > takes place, so I don't think it should interact with type checking
| > at all.
| >
| > I don't think this normalisation should include type families,
| > although H98 type synonyms are a kind of degenerate case of type
| > families.
| >
| > Would that design resolve this particular issue?
|
| Not quite, but it refines my proposal of requiring that type synonyms
| in the rhs of type instances need to be saturated.  Let me elaborate.

Why not quite?

| So, the crucial point is that, as you wrote,
|
| > I don't think this normalisation should include type families,
| > although H98 type synonyms are a kind of degenerate case of type
| > families.

Exactly!   Just to state it more clearly again:

Any programmer-written type (i.e one forming part
of the source text of the program) must obey the
following rules:
- well-kinded
- type synonyms saturated
- arguments of type applications are monotypes
(but -> is special)

However these rules are checked ONLY AFTER EXPANDING
SATURATE TYPE SYNONYMS (but doing no reduction on
type families)

OK, let's try the examples Manuel suggests:

| The current implementation is wrong, as it permits
|
|type S a b = a
|type family F a :: * -> *
|type instance F a = S a

This is illegal because a programmer-written type (the (S a) on the rhs) is an 
unsaturated type synonym.

|type S a b = a
|type family F (a :: * -> *) b :: * -> *
|type instance F a b = S (S a) b b

This is legal because the programmer-written type (S (S a) b b) can
be simplified to 'a' by expanding type synonyms.


The above checks are performed by checkValidType in TcMType.  In particular, 
the check for saturated synonyms is in check_type (line 1134 or thereabouts).  
I'm not sure why these checks are not firing for the RHS of a type family 
declaration.  Maybe we aren't calling checkValidType on it.

So I think we are agreed.  I think the above statement of validity should 
probably appear in the user manual.

Simon
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Hugo Pacheco:
Since I was the one to start this thread, I have managed to  
implement what I initially wanted as F a :: *->* with F a x::*, and  
the cost of not having partially applied type synonyms was not much  
apart from some more equality coercions that I wasn't expecting.

[..]

Generally, I love type-indexed types.

Glad to hear that!

Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Claus Reinke]

Well, we still need normal subject reduction (i.e., types don't change  
under value term reduction), and we have established that for System  
FC (in the TLDI paper).


In addition, type term normalisation (much like value term  
normalisation) needs to be confluent; otherwise, you won't get a  
complete type inference/checking algorithm.


if you have separate rules for generating constraints (decomposition)
and type term normalisation, that also needs to include confluence
of the combined system, which was the issue here, i believe.


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.


System FC as described in the paper is GHC's current Core language.   
What are you missing?


for now, interaction with pre-Core features, such as generalised type
synonyms?-) i just tend to program in ghc Front, not ghc Core;-)

later, there'll be other fun, eg, my extensible record code depends 
on ghc's particular interpretation of the interaction between FDs 
and overlap resolution, much of Oleg's code depends on a trick 
that he has isolated in a small group of type equality predicates,

carefully exploiting ghc's ideosynchrasies. neither his nor my code
works in hugs, even though we nominally use language features
supported by both ghc and hugs, even originating in hugs. 

probably, closed type families can provide better answers to these 
issues, but until they are here, and their interaction with other ghc 
type system features has been studied, the idea of mapping FDs 
to type families has to be taken with a grain of salt, i guess. as
with FDs, it isn't a single feature that causes trouble, it is the 
interaction of many features, combined with real-life programs

that stretch the language boundaries they run into.

I don't think we can avoid losing that expressiveness, as you  
demonstrated that it leads to non-confluence of type term  
normalisation - see also my reply to SimonPJ's message in this thread.


i know that we sometimes have to give up features that look
nice but have hidden traps - that doesn't mean i have to like
it, though!-)

Haskell always had the decomposition rule.  Maybe we confused the  
matter, by always showing a particular instance of the decomposition  
rule, rather than the general rule.  Here it is in all it's glory:


  t1 t2 ~ t1' t2'  <==>  t1 ~ t1', t2 ~ t2'

No mention of a type family.  However, the rule obviously still needs  
to be correct if we allow any of the type terms (including t1 and t1')  
to include *saturated* applications of type families.


before type families, t1 and t1' were straightforward type constructors 
(unless you include type synonyms, for which the decomposition doesn't
apply). with type families, either may be a type-level function, and 
suddenly it looks as if you are matching on a function application.


compare the expression-level:

   f (Just x) = x -- ok, because 'Just x' is irreducible

   g (f x) = x -- oops?

so what i was missing was that you had arranged matters to
exclude some problematic cases from that decomposition rule:

- partially applied type synonyms (implicitly, by working in core)
- partially applied (in terms of type indices) type families (by a 
   side condition not directly visible in the rule system)


in other words, the rule looks too general for what you
had in mind, not too specific!-)

claus


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Simon Peyton-Jones:

| > * GHC says that these constraints must be obeyed only
| >*after* the programmer-written type has been normalised
| >by expanding saturated type synonyms
| >
...
| > I regard this as a kind of pre-pass, before serious type checking
| > takes place, so I don't think it should interact with type  
checking

| > at all.
| >
| > I don't think this normalisation should include type families,
| > although H98 type synonyms are a kind of degenerate case of type
| > families.
| >
| > Would that design resolve this particular issue?
|
| Not quite, but it refines my proposal of requiring that type  
synonyms
| in the rhs of type instances need to be saturated.  Let me  
elaborate.


Why not quite?


Maybe I was thinking too much in terms of GHC's implementation, but  
due to the lazy expansion type synonyms, the expansion is interleaved  
with all the rest of type checking.  But I think I now know what you  
meant: the outcome should be *as if* type synonym expansion was done  
as a pre-pass.



| So, the crucial point is that, as you wrote,
|
| > I don't think this normalisation should include type families,
| > although H98 type synonyms are a kind of degenerate case of type
| > families.

Exactly!   Just to state it more clearly again:

   Any programmer-written type (i.e one forming part
   of the source text of the program) must obey the
   following rules:
   - well-kinded
   - type synonyms saturated
   - arguments of type applications are monotypes
   (but -> is special)

   However these rules are checked ONLY AFTER EXPANDING
   SATURATE TYPE SYNONYMS (but doing no reduction on
   type families)


I agree.

The above checks are performed by checkValidType in TcMType.  In  
particular, the check for saturated synonyms is in check_type (line  
1134 or thereabouts).  I'm not sure why these checks are not firing  
for the RHS of a type family declaration.  Maybe we aren't calling  
checkValidType on it.


I'll check that.  Might be an oversight.

So I think we are agreed.  I think the above statement of validity  
should probably appear in the user manual.


Yes, I'll take care of that.

Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

RE: [Haskell-cafe] Equality constraints in type families

[Simon Peyton-Jones]

| > Why not quite?
|
| Maybe I was thinking too much in terms of GHC's implementation, but
| due to the lazy expansion type synonyms, the expansion is interleaved
| with all the rest of type checking.  But I think I now know what you
| meant: the outcome should be *as if* type synonym expansion was done
| as a pre-pass.

Well, validity checking is done when (and only when) converting an HsType to a 
Type.  (The former being a programmer written type.)  That's just what we want. 
 It's done by checkValidType, which is not at all interleaved.  Once that check 
is done, the lazy expansion can, I think, be left to itself; no further 
checking is required.

Simon
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Hugo Pacheco]

>
> The current implementation is wrong, as it permits
>
>   type S a b = a
>   type family F a :: * -> *
>   type instance F a = S a
>
> Why do we need to forbid this type instance?  Because it breaks the
> confluence of equality constraint normalisation.  Here are two
> diverging normalisations:
>
>   (1)
>
> F Int Bool  ~  F Int Char
>
>   ==> DECOMP
>
> F Int ~ F Int, Bool ~ Char
>
>   ==> FAIL
>
>
>   (2)
>
> F Int Bool  ~  F Int Char
>
>   ==> TOP
>
> S Int Bool  ~  S Int Char
>
>   ==> (expand type synonym)
>
> Int  ~  Int
>
>   ==> TRIVIAL
>
> This does mean that a program such as

type FList a = Either One ((,) a)
type instance F [a] = FList a

will be disallowed in further versions?
Doesn't this problem occur only for type synonyms that ignore one or more of
the parameters? If so, this could be checked...

hugo
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Hugo Pacheco]

Sorry, I meant

type FList a x = Either One (a,x)
type instance F [a] = FList a

On Thu, Mar 27, 2008 at 4:45 PM, Hugo Pacheco <[EMAIL PROTECTED]> wrote:

>
>
> > The current implementation is wrong, as it permits
> >
> >   type S a b = a
> >   type family F a :: * -> *
> >   type instance F a = S a
> >
> > Why do we need to forbid this type instance?  Because it breaks the
> > confluence of equality constraint normalisation.  Here are two
> > diverging normalisations:
> >
> >   (1)
> >
> > F Int Bool  ~  F Int Char
> >
> >   ==> DECOMP
> >
> > F Int ~ F Int, Bool ~ Char
> >
> >   ==> FAIL
> >
> >
> >   (2)
> >
> > F Int Bool  ~  F Int Char
> >
> >   ==> TOP
> >
> > S Int Bool  ~  S Int Char
> >
> >   ==> (expand type synonym)
> >
> > Int  ~  Int
> >
> >   ==> TRIVIAL
> >
> > This does mean that a program such as
>
> type FList a = Either One ((,) a)
> type instance F [a] = FList a
>
> will be disallowed in further versions?
> Doesn't this problem occur only for type synonyms that ignore one or more
> of the parameters? If so, this could be checked...
>
> hugo
>
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Wolfgang Jeltsch]

Am Mittwoch, 26. März 2008 03:07 schrieb Hugo Pacheco:
> > The extra syntax has its advantages (more local information) and
> > disadvantages (more clutter).  We weren't convinced that we need the
> > extra syntax, so left it out for the moment. However, this is
> > something that can always be changed if experience shows that programs
> > are easier to understand with extra syntax.  It doesn't affect the
> > type theory and is really a pure language design question.  I'd be
> > glad to hear some more opinions about this matter.
>
> I would go for the braces as Claus suggested,

I would do so, too.

Best wishes,
Wolfgang
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Wolfgang Jeltsch]

Am Donnerstag, 27. März 2008 22:43 schrieb Wolfgang Jeltsch:
> Am Mittwoch, 26. März 2008 03:07 schrieb Hugo Pacheco:
> > > The extra syntax has its advantages (more local information) and
> > > disadvantages (more clutter).  We weren't convinced that we need the
> > > extra syntax, so left it out for the moment. However, this is
> > > something that can always be changed if experience shows that programs
> > > are easier to understand with extra syntax.  It doesn't affect the
> > > type theory and is really a pure language design question.  I'd be
> > > glad to hear some more opinions about this matter.
> >
> > I would go for the braces as Claus suggested,
>
> I would do so, too.

Hmm, but then we should also introduce braces for ordinary type synonyms:

type ReaderWriterT m = ReaderT (WriterT m)

x :: {ReaderWriterT IO} Char

> […]

Best wishes,
Wolfgang
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Hugo Pacheco]

The reason for the braces in type families is because type indices are
treated differently than normal parameters. I don't think this should be
adopted for type synonyms either.

Cheers,
hugo

On Thu, Mar 27, 2008 at 9:48 PM, Wolfgang Jeltsch <
[EMAIL PROTECTED]> wrote:

> Am Donnerstag, 27. März 2008 22:43 schrieb Wolfgang Jeltsch:
> > Am Mittwoch, 26. März 2008 03:07 schrieb Hugo Pacheco:
> > > > The extra syntax has its advantages (more local information) and
> > > > disadvantages (more clutter).  We weren't convinced that we need the
> > > > extra syntax, so left it out for the moment. However, this is
> > > > something that can always be changed if experience shows that
> programs
> > > > are easier to understand with extra syntax.  It doesn't affect the
> > > > type theory and is really a pure language design question.  I'd be
> > > > glad to hear some more opinions about this matter.
> > >
> > > I would go for the braces as Claus suggested,
> >
> > I would do so, too.
>
> Hmm, but then we should also introduce braces for ordinary type synonyms:
>
>type ReaderWriterT m = ReaderT (WriterT m)
>
>x :: {ReaderWriterT IO} Char
>
> > […]
>
> Best wishes,
> Wolfgang
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Hugo Pacheco:

Sorry, I meant

type FList a x = Either One (a,x)
type instance F [a] = FList a


We should not allow such programs.

Manuel




On Thu, Mar 27, 2008 at 4:45 PM, Hugo Pacheco <[EMAIL PROTECTED]>  
wrote:



The current implementation is wrong, as it permits

  type S a b = a
  type family F a :: * -> *
  type instance F a = S a

Why do we need to forbid this type instance?  Because it breaks the
confluence of equality constraint normalisation.  Here are two
diverging normalisations:

  (1)

F Int Bool  ~  F Int Char

  ==> DECOMP

F Int ~ F Int, Bool ~ Char

  ==> FAIL


  (2)

F Int Bool  ~  F Int Char

  ==> TOP

S Int Bool  ~  S Int Char

  ==> (expand type synonym)

Int  ~  Int

  ==> TRIVIAL

This does mean that a program such as

type FList a = Either One ((,) a)
type instance F [a] = FList a

will be disallowed in further versions?
Doesn't this problem occur only for type synonyms that ignore one or  
more of the parameters? If so, this could be checked...


hugo




___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Hugo Pacheco]

Yes, but doesn't the confluence problem only occur for type synonyms that
ignore one or more of the parameters? If so, this could be checked...

On Fri, Mar 28, 2008 at 12:04 AM, Manuel M T Chakravarty <
[EMAIL PROTECTED]> wrote:

> Hugo Pacheco:
> > Sorry, I meant
> >
> > type FList a x = Either One (a,x)
> > type instance F [a] = FList a
>
> We should not allow such programs.
>
> Manuel
>
> >
> >
> > On Thu, Mar 27, 2008 at 4:45 PM, Hugo Pacheco <[EMAIL PROTECTED]>
> > wrote:
> >
> >
> > The current implementation is wrong, as it permits
> >
> >   type S a b = a
> >   type family F a :: * -> *
> >   type instance F a = S a
> >
> > Why do we need to forbid this type instance?  Because it breaks the
> > confluence of equality constraint normalisation.  Here are two
> > diverging normalisations:
> >
> >   (1)
> >
> > F Int Bool  ~  F Int Char
> >
> >   ==> DECOMP
> >
> > F Int ~ F Int, Bool ~ Char
> >
> >   ==> FAIL
> >
> >
> >   (2)
> >
> > F Int Bool  ~  F Int Char
> >
> >   ==> TOP
> >
> > S Int Bool  ~  S Int Char
> >
> >   ==> (expand type synonym)
> >
> > Int  ~  Int
> >
> >   ==> TRIVIAL
> >
> > This does mean that a program such as
> >
> > type FList a = Either One ((,) a)
> > type instance F [a] = FList a
> >
> > will be disallowed in further versions?
> > Doesn't this problem occur only for type synonyms that ignore one or
> > more of the parameters? If so, this could be checked...
> >
> > hugo
> >
> >
>
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Wolfgang Jeltsch]

Am Donnerstag, 27. März 2008 23:12 schrieben Sie:
> The reason for the braces in type families is because type indices are
> treated differently than normal parameters. I don't think this should be
> adopted for type synonyms either.
>
> Cheers,
> hugo

In a way, there is also different treatment in the case of type synonyms.  If 
you have the definition

type ReaderWriterT m = ReaderT (WriterT m),

you cannot leave out the m but you can leave out the result type parameter.

I think, it would be good if the syntax of type synonyms and type synonym 
families was consistent.

Best wishes,
Wolfgang
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Hugo Pacheco:
Yes, but doesn't the confluence problem only occur for type synonyms  
that ignore one or more of the parameters? If so, this could be  
checked...


You can't check this easily (for the general case).

Given

  type family G a b
  type FList a x = G a x
  type instance F [a] = FList a

Does FList ignore its second argument?  Depends on the type instances  
of G.


Manuel




On Fri, Mar 28, 2008 at 12:04 AM, Manuel M T Chakravarty <[EMAIL PROTECTED] 
> wrote:

Hugo Pacheco:
> Sorry, I meant
>
> type FList a x = Either One (a,x)
> type instance F [a] = FList a

We should not allow such programs.

Manuel

>
>
> On Thu, Mar 27, 2008 at 4:45 PM, Hugo Pacheco <[EMAIL PROTECTED]>
> wrote:
>
>
> The current implementation is wrong, as it permits
>
>   type S a b = a
>   type family F a :: * -> *
>   type instance F a = S a
>
> Why do we need to forbid this type instance?  Because it breaks the
> confluence of equality constraint normalisation.  Here are two
> diverging normalisations:
>
>   (1)
>
> F Int Bool  ~  F Int Char
>
>   ==> DECOMP
>
> F Int ~ F Int, Bool ~ Char
>
>   ==> FAIL
>
>
>   (2)
>
> F Int Bool  ~  F Int Char
>
>   ==> TOP
>
> S Int Bool  ~  S Int Char
>
>   ==> (expand type synonym)
>
> Int  ~  Int
>
>   ==> TRIVIAL
>
> This does mean that a program such as
>
> type FList a = Either One ((,) a)
> type instance F [a] = FList a
>
> will be disallowed in further versions?
> Doesn't this problem occur only for type synonyms that ignore one or
> more of the parameters? If so, this could be checked...
>
> hugo
>
>




___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Hugo Pacheco]

On Sun, Mar 30, 2008 at 3:54 AM, Manuel M T Chakravarty <
[EMAIL PROTECTED]> wrote:

> Hugo Pacheco:
> > Yes, but doesn't the confluence problem only occur for type synonyms
> > that ignore one or more of the parameters? If so, this could be
> > checked...
>
> You can't check this easily (for the general case).
>

I was most interested in knowing that this assumption was enough, and it
looks like it does.


>
> Given
>
>   type family G a b
>type FList a x = G a x
>type instance F [a] = FList a
>
> Does FList ignore its second argument?  Depends on the type instances
> of G.
>
> Manuel
>

I haven't thought of that, thanks for the example.

hugo
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Hugo Pacheco]

Anyway, do you think it is feasible to have a flag such as
-fallow-unsafe-type-families for users to use at their own risk? (supposing
we know how to guarantee these constraints).
I speak for my own, there are currently some nice thinks that I can only
accomplish with partially applied type synonyms in type families, otherwise
code starts to get dummier in terms of type contexts and context variables.

Thanks,
hugo

On Sun, Mar 30, 2008 at 4:14 AM, Hugo Pacheco <[EMAIL PROTECTED]> wrote:

> On Sun, Mar 30, 2008 at 3:54 AM, Manuel M T Chakravarty <
> [EMAIL PROTECTED]> wrote:
>
> > Hugo Pacheco:
> > > Yes, but doesn't the confluence problem only occur for type synonyms
> > > that ignore one or more of the parameters? If so, this could be
> > > checked...
> >
> > You can't check this easily (for the general case).
> >
>
> I was most interested in knowing that this assumption was enough, and it
> looks like it does.
>
>
> >
> > Given
> >
> >   type family G a b
> >type FList a x = G a x
> >type instance F [a] = FList a
> >
> > Does FList ignore its second argument?  Depends on the type instances
> > of G.
> >
> > Manuel
> >
>
> I haven't thought of that, thanks for the example.
>
> hugo
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Equality constraints in type families

[Manuel M T Chakravarty]

Hugo Pacheco:
Anyway, do you think it is feasible to have a flag such as -fallow- 
unsafe-type-families for users to use at their own risk? (supposing  
we know how to guarantee these constraints).


Sorry, but it doesn't seem like a good idea to enable an unsound type  
system even by an explicit option.


Manuel

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe