Mark P Jones writes:
[Sorry, I guess this should have been in the cafe ...]
Simon Peyton-Jones wrote:
The trouble is that
a) the coverage condition ensures that everything is well behaved
b) but it's too restrictive for some uses of FDs, notably the MTL library
c) there are many
Sorry, forgot to add
[2]
http://www.comp.nus.edu.sg/~sulzmann/publications/jfp-fds-revised.pdf
Martin
Martin Sulzmann writes:
Mark P Jones writes:
[Sorry, I guess this should have been in the cafe ...]
Simon Peyton-Jones wrote:
The trouble is that
a) the coverage
Simon Peyton-Jones writes:
| I believe that this weak coverage condition (which is also called
| the dependency condition somewhere on the wiki) is exactly what GHC
| 6.4 used to implement but than in 6.6 this changed. According to
| Simon's comments on the trac ticket, this rule requires
Manuel M T Chakravarty writes:
Ross Paterson wrote,
On Tue, Oct 16, 2007 at 10:56:27AM +1000, Manuel M T Chakravarty wrote:
Lennart Augustsson wrote,
And Haskell embedded a logical programming language on accident.
Well, we are just trying to fix that :)
Since types are
Iavor Diatchki writes:
Hello,
On 10/19/07, Martin Sulzmann [EMAIL PROTECTED] wrote:
Simon Peyton-Jones writes:
...
Like you, Iavor, I find it very hard to internalise just why (B) and
(C) are important. But I believe the paper gives examples of why they
are, and Martin
Constraint Handling Rules
Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones and Peter
J. Stuckey
In Journal of Functional Programming, 2007
Martin
Stop reading now unless you're really interested in the details!
I'm going to start by explaining some key (but hopefully
unsurprising) ideas before I
Slides (in pdf) are now available online:
http://taichi.ddns.comp.nus.edu.sg/taichiwiki/SingHaskell2007
http://www.comp.nus.edu.sg/~sulzmann/singhaskell07/index.html
- Tom Martin
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
Josef Svenningsson writes:
On Dec 28, 2007 11:40 PM, Mitar [EMAIL PROTECTED] wrote:
Would not it be interesting and useful (but not really efficient) to
have patterns something like:
foo :: Eq a = a - ...
foo (_{4}'b') = ...
which would match a list with four elements ending
). But we have no formal type
system for fundeps that describes this, and GHC's implementation certainly
rejects it.
Martin Sulzmann, Jeremy
Waznyhttp://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wazny:Jeremy.html,
Peter J.
Stuckeyhttp://www.informatik.uni-trier.de/%7Eley/db/indices
Not distributed (yet) but concurrent:
http://hackage.haskell.org/package/actor
The paper Actors with Multi-headed Message Receive Patterns. COORDINATION
2008http://www.informatik.uni-trier.de/%7Eley/db/conf/coordination/coordination2008.html#SulzmannLW08:
describes the design rationale.
Cheers,
[EMAIL PROTECTED] writes:
There is a great temptation to read the following declarations
class Pred a b
instance (Ord b, Eq b) = Pred [Int] b
instance Pred Bool Bool
as a Prolog program:
pred([int],B) - ord(B),eq(B).
pred(bool,bool).
(In
Some Haskell-STM benchmarks can be found here:
Dissecting Transactional Executions in Haskell
Cristian Perfumo et al
http://www.cs.rochester.edu/meetings/TRANSACT07/
Martin
-Willem Maessen writes:
On Mar 1, 2008, at 6:41 PM, Tom Davies wrote:
I'm experimenting with STM (in CAL[1]
The point is that Mark proposes a *pessimistic* ambiguity check whereas
Tom (as well as GHC) favors
an *optimistic* ambiguity check.
By pessimistic I mean that we immediately reject a program/type if
there's a potential
unambiguity. For example,
class Foo a b
forall a b. Foo a b = b - b
Manuel said earlier that the source of the problem here is foo's
ambiguous type signature
(I'm switching back to the original, simplified example).
Type checking with ambiguous type signatures is hard because the type
checker has to guess
types and this guessing step may lead to too many
that this was a mistake.
To summarize: I don't care if the definition is useless, I want to be
able to give it a type signature anyway.
(It's also pretty easy to fix the problem.)
-- Lennart
On Wed, Apr 9, 2008 at 7:20 AM, Martin Sulzmann
[EMAIL PROTECTED] mailto:[EMAIL PROTECTED] wrote:
Manuel said
Claus Reinke wrote:
type family Id a
type instance Id Int = Int
foo :: Id a - Id a
foo = id n
foo' :: Id a - Id a
foo' = foo
type function notation is slightly misleading, as it presents
qualified polymorphic types in a form usually reserved for unqualified
polymorphic types.
rewriting
Claus Reinke wrote:
The point is that the GHC type checker relies on automatic inference.
Hence, there'll
always be cases where certain reasonable type signatures are rejected.
..
To conclude, any system with automatic inference will necessary
reject certain type signatures/instances
in
Lennart Augustsson wrote:
On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann
[EMAIL PROTECTED] mailto:[EMAIL PROTECTED] wrote:
Lennart, you said
(It's also pretty easy to fix the problem.)
What do you mean? Easy to fix the type checker, or easy to fix the
program
We're also looking for (practical) examples of multi-range functional
dependencies
class C a b c | c - a b
Notice that there are multiple (two) parameters in the range of the FD.
It's tempting to convert the above to
class C a b c | c - a, c - b
but this yields a weaker (in terms of type
Mark P Jones wrote:
Martin Sulzmann wrote:
We're also looking for (practical) examples of multi-range
functional dependencies
class C a b c | c - a b
Notice that there are multiple (two) parameters in the range of the FD.
It's tempting to convert the above to
class C a b c | c - a, c - b
Sittampalam, Ganesh wrote:
Martin Sulzmann wrote:
Mark P Jones wrote:
In fact, the two sets of dependencies that you have given here are
provably equivalent, so it would be decidedly odd to have a type
improvement system that distinguishes between them.
Based
Sittampalam, Ganesh wrote:
Why not instead transform single-range FDs into multi-range ones where
possible?
That's a perfectly reasonable assumption and would establish the logical
property that
a - b /\ a - c iff a - b /\ c
for FDs (by definition).
Iavor Diatchki wrote:
Hello,
On Wed, Apr 16, 2008 at 11:06 PM, Martin Sulzmann
[EMAIL PROTECTED] wrote:
3) Multi-range FDs
Consider
class C a b c | a - b c
instance C a b b = C [a] [b] [b]
This time it's straightforward.
C [x] y z yields the improvement y = [b] and z = [b]
which
Iavor Diatchki wrote:
Hello,
On Thu, Apr 17, 2008 at 10:26 AM, Martin Sulzmann
[EMAIL PROTECTED] wrote:
leads to an instance improvement/instance improvement conflict,
like in the single-range FD case
class D a b | a - b
instance D a a = D [a] [a]
instance D [Int] Char
Sorry
Lennart Augustsson wrote:
To reuse a favorite word, I think that any implementation that
distinguishes 'a - b, a - c' from 'a - b c' is broken. :)
It does not implement FD, but something else. Maybe this something
else is useful, but if one of the forms is strictly more powerful than
the
does of course NOT hold. That is,
the combination of improvement rules derived from a - b and a - c
is NOT equivalent to the improvement rules derived from a - b c.
Logically, the equivalence obviously holds.
Martin
Iavor Diatchki wrote:
Hello,
On Thu, Apr 17, 2008 at 12:05 PM, Martin
Lennart Augustsson wrote:
I've never thought of one being shorthand for the other, really.
Since they are logically equivalent (in my interpretation) I don't
really care which one we regard as more primitive.
True. See my response to Iavor's recent email.
Martin
to.
In general, we need an infinite rules of the form
D a b, D [a]^k c == c = [b]^k
where
[a]^k stands for the k nested list [ ... [a] ... ]
The FD-CHR approach therefore proposes to use
D [a] c == c = [b]
which is a stronger rule (that is, is not a logical consequence).
Martin
Martin Sulzmann wrote
On Tue, Oct 13, 2009 at 9:37 AM, Simon Peyton-Jones
simo...@microsoft.comwrote:
| Is there any way to define type-level multiplication without requiring
| undecidable instances?
|
| No, not at the moment. The reasons are explained in the paper Type
| Checking with Open Type Functions
On Wed, Oct 14, 2009 at 7:33 AM, o...@okmij.org wrote:
Martin Sulzmann wrote:
Undecidable instances means that there exists a program for which
there's
an infinite reduction sequence.
I believe this may be too strong of a statement. There exists patently
terminating type families
The statements
class Cl [a] = Cl a
and
instance Cl a = Cl [a]
(I omit the type family constructor in the head for simplicyt)
state the same (logical) property:
For each Cl t there must exist Cl [t].
Their operational meaning is different under the dictionary-passing
translation [1].
The
On Fri, Jan 29, 2010 at 8:56 AM, o...@okmij.org wrote:
Here is a bit more simplified version of the example. The example has
no value level recursion and no overt recursive types, and no impredicative
polymorphism. The key is the observation, made earlier, that two types
c (c ()) and
Hi,
I wouldn't call this a bug, overlapping instances
and in particular the combination with functional dependencies
are something which is not well studied yet.
Hence, GHC is very conservative here.
I feel like you, this program should work.
As you correctly point out, there's a conflict among
Simon's dead right, too :) The issue raised here is of general nature and
doesn't depend on the particular (syntactic) formalism used to specify
type dependencies (let it be FDs, ATs,...). The consequence is that
instances and type dependencies are closer linked to each other
then one might think
This is still an ad-hoc solution, cause you lose
the `most-specific' instance property. You really have to
impose a `fixed' ordering in which instance-improvement rules
fire.
Recap:
The combination of overlapping instances
and type improvement leads to a `non-confluent' system, i.e.
there're
Very interesting Conor. Do you know Xi et al's APLAS'03 paper?
(Hongwei, I'm not sure whether you're on this list).
Xi et al. use GRDTs (aka GADTs aka first-class phantom types)
to represent XML documents. There're may be some connections
between what you're doing and Xi et al's work.
I believe
Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215
Email: [EMAIL PROTECTED]
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)
On Mon, 17 Oct 2005, Martin Sulzmann wrote:
Very interesting
Stefan Wehr writes:
Niklas Broberg [EMAIL PROTECTED] wrote::
On 2/10/06, Ross Paterson [EMAIL PROTECTED] wrote:
On Fri, Feb 10, 2006 at 05:20:47PM +0100, Niklas Broberg wrote:
- when looking at the definition of MonadWriter the Monoid constraint
is not strictly necessary, and
Stefan Wehr writes:
Martin Sulzmann [EMAIL PROTECTED] wrote::
Stefan Wehr writes:
[...]
Manuel (Chakravarty) and I agree that it should be possible to
constrain associated type synonyms in the context of class
definitions. Your example shows that this feature is actually
Claus Reinke writes:
The main argument for ATS is that the extra parameter for the
functionally dependend type disappears, but as you say, that
should be codeable in FDs. I say should be, because that does
not seem to be the case at the moment.
My approach for trying the encoding was
Workshop,
volume = 1865,
series = LNAI,
publisher = Springer-Verlag,
year = 2000
}
Martin
[EMAIL PROTECTED] writes:
Martin Sulzmann wrote:
- The type functions are obviously terminating, e.g.
type T [a] = [[a]] clearly terminates
[EMAIL PROTECTED] writes:
Let's consider the general case (which I didn't describe in my earlier
email).
In case we have an n-ary type function T (or (n+1)-ary type class
constraint T) the conditions says for each
type T t1 ... tn = t
(or rule T t1 ... tn x == t)
[EMAIL PROTECTED] writes:
Martin Sulzmann wrote:
Let's consider the general case (which I didn't describe in my earlier
email).
In case we have an n-ary type function T (or (n+1)-ary type class
constraint T) the conditions says for each
type T t1 ... tn = t
(or rule
is that each instance specifies its own
termination condition which can then be checked dynamically.
Possible but I haven't thought much about it. The simplest and most
efficient strategy seems to stop after n number of steps.
Martin
Roman Leshchinskiy writes:
On Mon, 27 Feb 2006, Martin Sulzmann
-
But I am still confused by the exact definition of coherence in the case
of
overlapping. Does the standard coherence theorem apply? If yes, how?
If no, is there a theorem?
Yes, the is, by Martin Sulzmann et al, the Theory of overloading (the
journal version)
http
Schrijvers writes:
On Thu, 13 Apr 2006, Martin Sulzmann wrote:
Coherence (roughly) means that the program's semantics is independent
of the program's typing.
In case of your example below, I could type the program
either use the first or the second instance (assuming
g has type Int
Coherence may also arise because of an ambiguous type.
Here's the classic example.
class Read a where read :: String - a
class Show a where show :: a - String
f s = show (read s)
f has type String-String, therefore we can pick
some arbitrary Read/Show classes.
If you want to know
Your example must loop because as you show below
the instance declaration leads to a cycle.
By black-holing you probably mean co-induction. That is,
if the statement to proven appears again, we assume it must hold.
However, type classes are by default inductive, so there's no
easy fix to offer to
2009/9/9 Stefan Holdermans ste...@cs.uu.nl
Dear Martin,
By black-holing you probably mean co-induction. That is,
if the statement to proven appears again, we assume it must hold.
However, type classes are by default inductive, so there's no
easy fix to offer to your problem.
A propos:
Harrison: A Simple Semantics for Polymorphic Recursion. APLAS 2005
is also related I think.
The ICFP'08 poster
Unified Type Checking for Type Classes and Type Families , Tom
Schrijvers and Martin Sulzmann
suggests that a type-passing semantics can even be programmed by
(mis)using type
in
terms of the source language.
I guess I also want it to be compositional, which I think is where
things break down.
-- Lennart
On Wed, Nov 12, 2008 at 2:26 PM, Martin Sulzmann
[EMAIL PROTECTED] wrote:
Lennart Augustsson wrote:
You can't write a straightforward dynamic semantics (in, say
[Discussion moved from Haskell to Haskell-Cafe]
Hi,
Regarding
- lazy overlap resolution aka unique instances
Well, if there's only instance which is not exported, then you can
use functional dependencies.
Assume
class C a
instance ... = C t
Internally, use
class C a | - a
instance ... = C
Hi,
let me answer your questions by comparing what's implemented in Chameleon.
(For details see
http://www.comp.nus.edu.sg/~sulzmann/chameleon/download/haskell.html#scoped)
QUESTION 1 -
In short, I'm considering adopting the Mondrian/Chameleon rule for GHC.
There are two
Lennart Augustsson writes:
[...]
But using functional dependencies feels like a sledge hammer,
and it is also not Haskell 98.
Well, I'm simply saying that your proposed extension which is not
Haskell 98 can be expressed in terms of a known type class extension.
I agree that
paper for references).
A formal result can be found here:
A Systematic Translation of Guarded Recursive Data Types to
Existential Types
by Martin Sulzmann and Meng Wang
http://www.comp.nus.edu.sg/~sulzmann/
Example encodings for some of the
examples we've seen so far can be found below.
Martin
55 matches
Mail list logo
