Comments see below.
On Wed, May 1, 2013 at 11:13 AM, AntC wrote:
>> Martin Sulzmann writes:
>>
>> (1) There's a mechanical way to translate FD programs with
>> non-overlapping instances to TF (and of course vice versa).
>
> Martin, no! no! no! You have comple
(1) There's a mechanical way to translate FD programs with
non-overlapping instances to TF (and of course vice versa). For
example, let's reconsider Oleg's example.
> {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE FlexibleContexts #-}
Any chance to express this in terms of a formal (constraint rewrite
framework).
For example, the Haskell rule, do *not* display implied superclasses,
can be
specified as follows. Consider the special case of
class Eq a
class Eq a => Ord a
Eq a, Ord a <=> Ord a
The above rule only applies
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
In more detail, here's the issue I see.
The AT inference system doesn't exhaustively apply all rules,
rather, the AT inferencer stops once we encounter a 'cycle'
such as T a = a where T is a type function constructor.
The important question is whether this will retain *complete* type
inference?
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.
> >
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.ha
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
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 i
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
Ross Paterson writes:
> On Mon, Apr 10, 2006 at 01:31:18PM +0800, Martin Sulzmann wrote:
> > You mention that nobody is really happy with FDs at the moment,
> > but you don't provide concrete arguments why. I assume you
> > refer to the following two issues:
>
Ross Paterson writes:
> (see the FunctionalDependencies page for background omitted here)
>
> One of the problems with the relaxed coverage condition implemented
> by GHC and Hugs is a loss of confluence. Here is a slightly cut-down
> version of Ex. 18 from the FD-CHR paper:
>
> clas
Manuel M T Chakravarty writes:
> Simon Peyton-Jones:
> > My current take, FWIW.
> >
> > [...]
> > Tentative conclusion: H' should have MPTC + FDs, but not ATs.
>
> My conclusion is that we should not include FDs or ATs into the standard
> at the moment. Standardising FDs as a stopgap me
Manuel M T Chakravarty writes:
> > Another thing, here's an excerpt of the current summary of the MPTC
> > dilemma from
> > http://haskell.galois.com/cgi-bin/haskell-prime/trac.cgi/wiki
> >
> >
> > Multi Parameter Type Classes Dilemma ¦
> >
> > Options for solving the dilemma ¦
>
a nice syntax for a specific kind of type class
programs. Though, as I've pointed out before any AT program can be
encoded with FDs but the other direction does not hold necessarily.
See the above paper for details.
Manuel M T Chakravarty writes:
> > -----
FYI, Chameleon supports a combination of lexically scoped
and partial type annotation. The latest Chameleon version
is a broken (fix on its way). Though, besides the implementation
there's also a concise formal description. See
[July 2005] Lexically Scoped Type Annotations
http://www.comp.nus.edu.
>
> > FYI, in a technical report version of the
> > FD paper, we already address such issues, briefly.
>
> where would I find that report?
>
http://www.comp.nus.edu.sg/~sulzmann/chr/download/fd-chr.ps.gz
See Section 5 and Appendix E.
Martin
_
Coverage is a sufficient condition to maintain termination. Though,
Coverage is also sufficient to maintain confluence. Hence, we
propose Weak Coverage which we know maintains confluence
under some conditions.
The main focus of the FD paper is how to restore confluence which is
important for com
It's very hard to follow you here. Can you formalize your proposal
below such that we can verify some formal results (e.g. tractable
inference, coherence etc).
Why not be "macho" and use a formal framework in which this all
can be expressed?
In one of your previous emails you said:
> ...make t
Check out Section 8.1. in
P. J. Stuckey and M. Sulzmann. A theory of overloading. ACM Transactions on
Programming Languages and Systems (TOPLAS), 27(6):1-54, 2005.
for how to use disequality constraints to "resolve" overlapping
instances.
BTW, the translation scheme in the above paper employs
ory of Overloading".
I claim that when it comes to unrestricted type class programming
CHRs are the way to go. CHRs have a clean semantic meaning and
precisely explain the meaning of type class programs.
Martin
Claus Reinke writes:
> > I'm forwarding an email that Martin Sulzmann
Ross Paterson writes:
> On Sat, Feb 18, 2006 at 12:26:36AM +, Ross Paterson wrote:
> > Martin Sulzmann <[EMAIL PROTECTED]> writes:
> > > Result2:
> > > Assuming we can guarantee termination, then type inference
> > > is complete if we can satisf
22 matches
Mail list logo
