Ryan Ingram wrote:
It believe that it's true that ((forall a. t a) - t') does not entail
(exists a. t a - t') in constructivist logic, but I can't come up
with a proof off the top of my head. Intuitively, to construct a
value of type (E t t') you need to fix an a, and I don't think it's
Wolfgang Jeltsch wrote:
First, I thought so too but I changed my mind. To my knowledge a type
(forall a. T[a]) - T' is equivalent to the type exists a. (T[a] - T'). It’s
the same as in predicate logic – Curry-Howard in action.
The connection is the other way round, I think.
(exists a.
On Tuesday 17 February 2009 7:28:18 am Heinrich Apfelmus wrote:
Wolfgang Jeltsch wrote:
First, I thought so too but I changed my mind. To my knowledge a type
(forall a. T[a]) - T' is equivalent to the type exists a. (T[a] - T').
It’s the same as in predicate logic – Curry-Howard in action.
On Tue, Feb 17, 2009 at 5:22 AM, Dan Doel dan.d...@gmail.com wrote:
-- fail: inferred type less polymorphic than expected
-- This seems like it could perhaps work, since E''
-- re-hides the 'a' but it doesn't, probably because there's
-- no way to type the enclosed lambda expression properly.
On Tuesday 17 February 2009 5:27:45 pm Ryan Ingram wrote:
On Tue, Feb 17, 2009 at 5:22 AM, Dan Doel dan.d...@gmail.com wrote:
-- fail: inferred type less polymorphic than expected
-- This seems like it could perhaps work, since E''
-- re-hides the 'a' but it doesn't, probably because
Peter Verswyvelen wrote:
I'm having trouble understanding the explanation of the meaning of the
signature of runST at
http://en.wikibooks.org/wiki/Haskell/Existentially_quantified_types
I could try to read the article a couple of times again, but are there any
other good readings about
