On 07-Jun-1999, S.D.Mechveliani <[EMAIL PROTECTED]> wrote:
> One more question on the program simplification and `bottom'.
>
> People say, that the transformations like x - x -> 0 :: Integer
> are hardly ever applicable, because x may occur `undefined'.
This issue was already resolved --
On Mon, 7 Jun 1999, S.D.Mechveliani wrote:
> One more question on the program simplification and `bottom'.
>
> People say, that the transformations like x - x -> 0 :: Integer
>
> are hardly ever applicable, because x may occur `undefined'.
There is another problem lurking here as well.
> There is another problem lurking here as well. Namely space issues.
> Consider the following program. It runs in constant space.
>
> let xs = 1..n
> x = head xs
> in x - x + last xs + x
>
> Now transforming it using
> M - M -> 0 and
> 0 + M -> M
> yields
>
> let xs = 1..n
> x = head
> >> {rules Num a=> x::a, y::[a] ==>
> x+y = [x]+y}
> >> instance Num a => Num [a] where ...
> >> one could expect for x :: Num b=>b the casting
> >> x + [x,y] -->
> [x] + [x,y]
> > Provided the two
Simon Peyton-Jones wrote:
>
> > Another question on *rules*.
> > Could they help the implicit type casting?
> > For example, with
> > {rules Num a=> x::a, y::[a] ==> x+y = [x]+y}
> > instance Num a => Num [a] where ...
> > one could expect for
> Another question on *rules*.
> Could they help the implicit type casting?
> For example, with
> {rules Num a=> x::a, y::[a] ==> x+y = [x]+y}
> instance Num a => Num [a] where ...
> one could expect for x :: Num b=>b the casting
>
I think that John Darlington's group at Imperial College were to first
to use rule driven program transformation in their various skelton/coordination
language parallelising compilers.
Here, Tore Bratvold used simple higher order function/composition
distribution transformation rules in his paral
Thanks to everyone who has contributed to the discussion about
transformation rules. There is clearly something inteeresting
going on here!
There is clearly a huge spectrum of possibilities, ranging from
nothing at all to a full theorem-proving system. In adding rules
to GHC I'm trying to star
Lennart Augustsson writes:
> Wolfram Kahl wrote:
>
> > In the end, my dreams even include a proof format
> > that can be checked by the compiler :-)
>
> Dependent types! That's all you need.
Absolutely!
I have read your Cayenne paper
( http://www.cs.chalmers.se/%7Eaugustss/cayenne/pape
Wolfram Kahl wrote:
> In the end, my dreams even include a proof format
> that can be checked by the compiler :-)
Dependent types! That's all you need.
--
-- Lennart
On Fri, 7 May 1999, S.D.Mechveliani wrote:
> Also D.Tweed <[EMAIL PROTECTED]> writes
>
> > [..] it may dramatically affect the size of expressions held
> > temporarily, eg
> >
> > tipsOfTheDay
> > = map addCopyrightLogo (map toUppercase (map addHaveANiceDay
> > [tip1,tip2,tip3,,t
At 10:08 -0700 1999/05/04, peter <[EMAIL PROTECTED]> wrote:
>Hans aberg writes:
>When a group is expressed as a class G having operations e, *, and -1,
>then implicitly (via well defined semantics), a group is a quadruple,
>so I don't think the quadruple need be explicit in the Haskell program.
>T
At 11:02 + 1999/05/03, Wolfram Kahl wrote:
>With respect to the new RULES mechanism presented by
>Simon Peyton Jones (Thu, 22 Apr 1999),
>Carsten Schultz <[EMAIL PROTECTED]> writes
> > [...]
> > > And what about algebraic simplification? Say,
> > The same applies to our beloved monads.
> > The
Hans aberg writes:
>
> For expressing algebraic relations, I think one can use universal algebra
> by factoring through the free universal algebra of a particular set of
> relations. For example, if one wants to state that a binary operator is
> commutative, one can say that is should be defin
Mark P Jones <[EMAIL PROTECTED]> writes:
>
...
>
> [Aside: As a general comment to all readers of the Haskell mailing
> list, perhaps I can suggest: if you've posted something to the list
> within the last two weeks, and it hasn't received the kind of
> response that you were expecting, then
I've seen a couple of messages now about Simon's proposal for
a RULES mechanism in Haskell, but it's clear that I've missed
several of the messages, including the original proposal. I
suspect this is a result of recent changes in the way that the
list is handled, which should be resolved by now.
With respect to the new RULES mechanism presented by
Simon Peyton Jones (Thu, 22 Apr 1999),
Carsten Schultz <[EMAIL PROTECTED]> writes
> [...]
> > And what about algebraic simplification? Say,
> The same applies to our beloved monads.
> The compiler could be told about the monad laws.
Somebo
Wolfram Kahl writes:
>
>
> One might even imagine extended instance declarations
> like the following:
>
> > instance Monad []
> > {-# PROOF
> > "Monad-rightId"
> > forall f.f >>= return
> > = concat (map return f)
> > = concat (map (:[]) f)
> > =
18 matches
Mail list logo
