On 15/09/2008, at 21:16, Simon Peyton-Jones wrote:
| > What would we like to write? Perhaps something like
| >
| > "myrule" forall (type t :: *->*) (f :: a->a) x.
| > from (tmap f (to x :: t a)) = map f (from (to x :: t a))
|
| Regardless of the syntax, I suspect x will have to be given a t
| > What would we like to write? Perhaps something like
| >
| > "myrule" forall (type t :: *->*) (f :: a->a) x.
| > from (tmap f (to x :: t a)) = map f (from (to x :: t a))
|
| Regardless of the syntax, I suspect x will have to be given a type as
| well here, as in (x :: a)?
No, that's easily
On 15/09/2008, at 20:05, Simon Peyton-Jones wrote:
What would we like to write? Perhaps something like
"myrule" forall (type t :: *->*) (f :: a->a) x.
from (tmap f (to x :: t a)) = map f (from (to x :: t a))
Regardless of the syntax, I suspect x will have to be given a type as
well her
on above is to re-use the keyword 'type'.
What do you think? Manuel may have an opinion too.
Incidentally, once the rule is parsed and typechecked, the simplifier will have
no trouble doing the right thing.
Simon
| -Original Message-
| From: Roman Leshchinskiy [mailto:[EMAIL PR
