Hello,
On 5/9/06, Stefan Wehr <[EMAIL PROTECTED]> wrote:
>> class C a
>> class F a where type T a
>> instance F [a] where type T [a] = a
>> class (C (T a), F a) => D a where m :: a -> Int
>> instance C a => D [a] where m _ = 42
But there is also the equality `T [Int] = Int
Iavor Diatchki <[EMAIL PROTECTED]> wrote::
> Hello,
>
> On 5/3/06, Stefan Wehr <[EMAIL PROTECTED]> wrote:
>> class C a
>> class F a where type T a
>> instance F [a] where type T [a] = a
>> class (C (T a), F a) => D a where m :: a -> Int
>> instance C a => D [a] where m _ = 42
>
Manuel M T Chakravarty <[EMAIL PROTECTED]> wrote::
> Stefan Wehr:
>> Manuel M T Chakravarty <[EMAIL PROTECTED]> wrote::
>>
>> > Martin Sulzmann:
>> >> Manuel M T Chakravarty writes:
>> >> > Martin Sulzmann:
>> >> > > A problem with ATs at the moment is that some terminating FD programs
>> >> >
Stefan Wehr:
> Manuel M T Chakravarty <[EMAIL PROTECTED]> wrote::
>
> > Martin Sulzmann:
> >> Manuel M T Chakravarty writes:
> >> > Martin Sulzmann:
> >> > > A problem with ATs at the moment is that some terminating FD programs
> >> > > result into non-terminating AT programs.
> >> > >
> >>
Ross Paterson writes:
> On Fri, May 05, 2006 at 08:42:12AM +0100, Simon Peyton-Jones wrote:
> > Alas, g simply discards its argument, so there are no further
> > constraints on 'a'. I think Martin would argue that type inference
> > should succeed with a=Bool, since there is exactly one soluti
On Fri, May 05, 2006 at 08:42:12AM +0100, Simon Peyton-Jones wrote:
> Alas, g simply discards its argument, so there are no further
> constraints on 'a'. I think Martin would argue that type inference
> should succeed with a=Bool, since there is exactly one solution. Is
> this an example of what
| Superclass implication is reversed when performing type inference.
| In the same way that instance reduction is reserved.
|
| Here's the example again.
|
| class C a
| class F a where
|type T a
| instance F [a] where
|type T [a] = [[[a]]]
| class C (T a) => D a
| ^
|
| The important question is whether this will retain *complete* type
| inference? For example, in case of type annotations we need to
| test for equivalence among constraints.
An excellent question. Here's an example, adapted from Ross:
class C a where
type Result a
der if you have anything in
> mind?
>
> http://www.haskell.org//pipermail/haskell-prime/2006-May/001514.html
>
> Simon
>
>
> | -Original Message-
> | From: [EMAIL PROTECTED]
> [mailto:[EMAIL PROTECTED] On Behalf Of
> | Ross Paterson
> | Sen
Manuel M T Chakravarty writes:
> Martin Sulzmann:
> > Manuel M T Chakravarty writes:
> > > Martin Sulzmann:
> > > > A problem with ATs at the moment is that some terminating FD programs
> > > > result into non-terminating AT programs.
> > > >
> > > > Somebody asked how to write the Mon
see also:
http://www.haskell.org//pipermail/haskell-prime/2006-March/000847.html
1. As Manuel explained, in the AT formulation it's possible to avoid
non-termination by suspending (leave unsolved) any equality constraint
of form (a = ty) where 'a' appears free in a type argument to an
associate
On Thu, May 04, 2006 at 02:00:33PM +0100, Simon Peyton-Jones wrote:
> Actually, it won't. The spec just says that the function is monomorphic
> in 'a'. That is, 'a' can be instantiated only one way. So if f is
> called, say (f True True), then that fixes 'a' to be Bool and all is
> well.
Oops.
not denying
that such a thing might exist, but I wonder if you have anything in
mind?
http://www.haskell.org//pipermail/haskell-prime/2006-May/001514.html
Simon
| -Original Message-
| From: [EMAIL PROTECTED]
[mailto:[EMAIL PROTECTED] On Behalf Of
| Ross Paterson
| Sent: 03 May 2006
| On Tue, May 02, 2006 at 12:26:48AM +0100, Ross Paterson wrote:
| > So the MR raises the reverse
| > question: can you be sure that every tautologous constraint is
reducible?
|
| I think the answer is no. Consider:
|
| class C a where
| type Result a
| method :
Hello,
On 5/3/06, Stefan Wehr <[EMAIL PROTECTED]> wrote:
class C a
class F a where type T a
instance F [a] where type T [a] = a
class (C (T a), F a) => D a where m :: a -> Int
instance C a => D [a] where m _ = 42
If you now try to derive "D [Int]", you get
||-
Manuel M T Chakravarty <[EMAIL PROTECTED]> wrote::
> Martin Sulzmann:
>> Manuel M T Chakravarty writes:
>> > Martin Sulzmann:
>> > > A problem with ATs at the moment is that some terminating FD programs
>> > > result into non-terminating AT programs.
>> > >
>> > > Somebody asked how to write
On Tue, May 02, 2006 at 12:26:48AM +0100, Ross Paterson wrote:
> So the MR raises the reverse
> question: can you be sure that every tautologous constraint is reducible?
I think the answer is no. Consider:
class C a where
type Result a
method :: a -> Resul
Iavor Diatchki:
> On 4/29/06, Manuel M T Chakravarty <[EMAIL PROTECTED]> wrote:
> > instance Mul a b => Mul a [b] where
> > type Result a [b] = [Result a b] -- second argument is
> > different
> > x .*. ys = map (x .*.) ys
> >
> > The arguments to the ATs,
Martin Sulzmann:
> Manuel M T Chakravarty writes:
> > Martin Sulzmann:
> > > A problem with ATs at the moment is that some terminating FD programs
> > > result into non-terminating AT programs.
> > >
> > > Somebody asked how to write the MonadReader class with ATs:
> > > http://www.haskell.o
Manuel M T Chakravarty writes:
> Martin Sulzmann:
> > A problem with ATs at the moment is that some terminating FD programs
> > result into non-terminating AT programs.
> >
> > Somebody asked how to write the MonadReader class with ATs:
> > http://www.haskell.org//pipermail/haskell-cafe/2006
Ross Paterson writes:
> Thanks for clarifying this.
>
> On Sat, Apr 29, 2006 at 05:49:16PM -0400, Manuel M T Chakravarty wrote:
> > So, we get the following type for f
> >
> > f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b]
> >
> > Given the instance definitions of t
On Sat, Apr 29, 2006 at 07:13:28PM -0400, Manuel M T Chakravarty wrote:
> 1. You are using non-standard instances with contexts containing
> non-variable predicates. (I am not disputing the potential
> merit of these, but we don't know whether they apply to Haskell'
>
Thanks for clarifying this.
On Sat, Apr 29, 2006 at 05:49:16PM -0400, Manuel M T Chakravarty wrote:
> So, we get the following type for f
>
> f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b]
>
> Given the instance definitions of that example, you can never satisfy
> the equal
Hello,
On 4/29/06, Manuel M T Chakravarty <[EMAIL PROTECTED]> wrote:
instance Mul a b => Mul a [b] where
type Result a [b] = [Result a b] -- second argument is
different
x .*. ys = map (x .*.) ys
The arguments to the ATs, in an instance def, need to co
Martin Sulzmann:
> A problem with ATs at the moment is that some terminating FD programs
> result into non-terminating AT programs.
>
> Somebody asked how to write the MonadReader class with ATs:
> http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html
>
> This requires an AT ext
Ross Paterson:
> To ensure termination with FDs, there is a proposed restriction that
> an instance that violates the coverage condition must have a trivial
> instance improvement rule. Is the corresponding restriction also
> required for ATs, namely that an associated type synonym definition
> ma
Ross Paterson:
> On Thu, Apr 27, 2006 at 12:40:47PM +0800, Martin Sulzmann wrote:
> > Yes, FDs and ATs have the exact same problems when it comes to termination.
> > The difference is that ATs impose a dynamic check (the occurs check)
> > when performing type inference (fyi, such a dynamic check is
Ross Paterson writes:
> On Thu, Apr 27, 2006 at 12:40:47PM +0800, Martin Sulzmann wrote:
> > Yes, FDs and ATs have the exact same problems when it comes to termination.
> > The difference is that ATs impose a dynamic check (the occurs check)
> > when performing type inference (fyi, such a dynam
On Thu, Apr 27, 2006 at 12:40:47PM +0800, Martin Sulzmann wrote:
> Yes, FDs and ATs have the exact same problems when it comes to termination.
> The difference is that ATs impose a dynamic check (the occurs check)
> when performing type inference (fyi, such a dynamic check is sketched
> in a TR ver
Yes, FDs and ATs have the exact same problems when it comes to termination.
The difference is that ATs impose a dynamic check (the occurs check)
when performing type inference (fyi, such a dynamic check is sketched
in a TR version of the FD-CHR paper).
A problem with ATs at the moment is that som
To ensure termination with FDs, there is a proposed restriction that
an instance that violates the coverage condition must have a trivial
instance improvement rule. Is the corresponding restriction also
required for ATs, namely that an associated type synonym definition
may only contain another as
31 matches
Mail list logo
