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] =
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
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
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
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)
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
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
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
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
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
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)
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
| * 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
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,
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
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
| 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
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
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
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,
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
| | 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
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 ~
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
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
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
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
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
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
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
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
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
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
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
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.
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
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
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
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
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
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
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
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
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 :: *
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
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:
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
47 matches
Mail list logo
