Dan Weston wrote:
What is it called if it's both?
Then we say the argument occurs in both positive and negative
positions or the argument occurs in both covariant and contravariant
positions. There doesn't seem to be a shorter name. I want to note that
this kind of thing drives OOP crazy.
On 4/5/07, Albert Y. C. Lai [EMAIL PROTECTED] wrote:
Dan Weston wrote:
What is it called if it's both?
Then we say the argument occurs in both positive and negative
positions or the argument occurs in both covariant and contravariant
positions. There doesn't seem to be a shorter name. I want
On Thu, Apr 05, 2007 at 06:26:17PM -0300, Felipe Almeida Lessa wrote:
I know that types like
data T = T (T - T)
are inhabitated by things other than bottom (like id or \_ -
undefined), but can it be useful for *anything*?
Yes. In particular, types like those can produce an explicit
Then we say the argument occurs in both positive and negative
positions or the argument occurs in both covariant and contravariant
positions. There doesn't seem to be a shorter name. I want to note that
this kind of thing drives OOP crazy.
i recall this paper being of some help:-)
Hey,
It is well-known that negative datatypes can be used to encode
recursion, without actually explicitly using recursion. As a little
exercise, I set out to define the fixpoint combinator using negative
datatypes. I think the result is kinda cool :) Comments are welcome :)
Edsko
{-
On Wed, Apr 04, 2007 at 07:39:24PM +0100, Edsko de Vries wrote:
Hey,
It is well-known that negative datatypes can be used to encode
recursion, without actually explicitly using recursion. As a little
exercise, I set out to define the fixpoint combinator using negative
datatypes. I think the
For those of us who aren't type theorists: What's a negative datatype?
Mike
Edsko de Vries wrote:
Hey,
It is well-known that negative datatypes can be used to encode
recursion, without actually explicitly using recursion. As a little
exercise, I set out to define the fixpoint combinator using
On Wed, Apr 04, 2007 at 01:36:18PM -0700, Michael Vanier wrote:
For those of us who aren't type theorists: What's a negative datatype?
Negative isn't the usual term; we mostly call them 'contravariantly
recursive' data types, due to CT influence. Anyways the thing to note
is that the value
What is it called if it's both? Is this even legal in Haskell? It seems
as though this would not be a grounded type, going on forever in both
directions.
Dan
Stefan O'Rear wrote:
On Wed, Apr 04, 2007 at 01:36:18PM -0700, Michael Vanier wrote:
For those of us who aren't type theorists:
On Wed, Apr 04, 2007 at 02:57:06PM -0700, Dan Weston wrote:
What is it called if it's both? Is this even legal in Haskell? It seems
as though this would not be a grounded type, going on forever in both
directions.
I guess negative datatype is being a bit loose with terminology; the
function
Edsko,
(Moved to Haskell Cafe.)
It is well-known that negative datatypes can be used to encode
recursion, without actually explicitly using recursion. As a little
exercise, I set out to define the fixpoint combinator using negative
datatypes. I think the result is kinda cool :) Comments are
Mike,
For those of us who aren't type theorists: What's a negative
datatype?
A type that has a recursive call in negative position. Negative
positions are the argument positions in function types. (But if a
function type appears in a negative position, then its own argument
position is
Yeah, it's rather cool. IIRC, this style of encoding of recursion
operators is attributed to Morris.
Do you have a reference?
Before the advent of equality coercions, GHC typically had problems
generating code for these kinds of definitions. Did you test this
with a release version?
Edsko,
Yeah, it's rather cool. IIRC, this style of encoding of recursion
operators is attributed to Morris.
Do you have a reference?
James H. Morris. Lambda calculus models of programming languages.
Technical Report MIT-LCS//MIT/LCS/TR-57, Massachusetts Institute of
Technology, 1968.
On Wed, Apr 04, 2007 at 11:05:51PM +0200, Stefan Holdermans wrote:
Edsko,
Yeah, it's rather cool. IIRC, this style of encoding of recursion
operators is attributed to Morris.
Do you have a reference?
James H. Morris. Lambda calculus models of programming languages.
Technical Report
Edsko,
James H. Morris. Lambda calculus models of programming languages.
Technical Report MIT-LCS//MIT/LCS/TR-57, Massachusetts Institute of
Technology, 1968.
Aah, I guess that's a bit old to be avaiable online :) Does he talk
about negative datatypes though? The Y combinator itself isn't
On Wed, Apr 04, 2007 at 11:15:25PM +0200, Stefan Holdermans wrote:
Edsko,
James H. Morris. Lambda calculus models of programming languages.
Technical Report MIT-LCS//MIT/LCS/TR-57, Massachusetts Institute of
Technology, 1968.
Aah, I guess that's a bit old to be avaiable online :) Does he
On Apr 4, 2007, at 5:01 PM, Edsko de Vries wrote:
Yeah, it's rather cool. IIRC, this style of encoding of recursion
operators is attributed to Morris.
Do you have a reference?
Before the advent of equality coercions, GHC typically had problems
generating code for these kinds of
18 matches
Mail list logo
