In the new type, the parameter 'a' is misleading. It has no connection to
the
'a's on the right of the equals sign. You might as well write:
type CB = forall a. a - a - a
On Tue, Jun 1, 2010 at 12:40 PM, Cory Knapp cory.m.kn...@gmail.com wrote:
Ah! That makes sense. Which raises a new
Thanks! That was exactly the sort of response I was looking for.
This explains why you need to double up for your current definitions. To
choose between two booleans (which will in turn allow you to choose between
'a's), you need a CB (CB a). You can eliminate the asymmetric type, though,
like
On Tue, Jun 1, 2010 at 12:40 PM, Cory Knapp cory.m.kn...@gmail.com wrote:
Thanks! That was exactly the sort of response I was looking for.
This explains why you need to double up for your current definitions. To
choose between two booleans (which will in turn allow you to choose
between
On Tue, Jun 1, 2010 at 3:40 PM, Cory Knapp cory.m.kn...@gmail.com wrote:
In the new type, the parameter 'a' is misleading. It has no connection to
the
'a's on the right of the equals sign. You might as well write:
type CB = forall a. a - a - a
Ah! That makes sense. Which raises a new
On Tuesday 01 June 2010 3:40:41 pm Cory Knapp wrote:
Note: this is universal quantification, not existential.
As I would assume. But I always see the forall keyword used when
discussing existential quantification. I don't know if I've ever seen an
exists keyword. Is there one? How would it
On Tuesday 01 June 2010 23:21:35, Dan Doel wrote:
I think SPJ is on record as saying it would add a lot of
complexity to the current GHC type system,
and I'm inclined to believe him.
In matters concerning the GHC type system, that's a fairly natural stance,
I think.
On Sat, May 29, 2010 at 9:28 PM, Cory Knapp cory.m.kn...@gmail.com wrote:
Hello,
A professor of mine was recently playing around during a lecture with
Church booleans (I.e., true = \x y - x; false = \x y - y) in Scala and
OCaml. I missed what he did, so I reworked it in Haskell and got this:
Jason Dagit wrote:
In Church's λ-calc the types are ignored,
Not so. Church-style lambda calculus is the one where types matter;
Curry-style is the one that ignores types and evaluates as if it were
the untyped lambda calculus.
Church encodings are based on the untyped LC rather than
On Sunday 30 May 2010 12:28:36 am Cory Knapp wrote:
type CB a = a - a - a
ct :: CB aC
ct x y = x
cf :: CB a
cf x y = y
cand :: CB (CB a) - CB a - CB a
cand p q = p q cf
cor :: CB (CB a) - CB a - CB a
cor p q = p ct q
The reason these types are required is that the 'a' in your
On Sun, May 30, 2010 at 4:08 AM, wren ng thornton w...@freegeek.org wrote:
Jason Dagit wrote:
In Church's λ-calc the types are ignored,
Not so. Church-style lambda calculus is the one where types matter;
Curry-style is the one that ignores types and evaluates as if it were the
untyped
Hello,
A professor of mine was recently playing around during a lecture with Church
booleans (I.e., true = \x y - x; false = \x y - y) in Scala and OCaml. I
missed what he did, so I reworked it in Haskell and got this:
type CB a = a - a - a
ct :: CB aC
ct x y = x
cf :: CB a
cf x y = y
cand ::
11 matches
Mail list logo
