[FoRK] Well... was Re: Uh oh. Retraction.

Jeff Bone jbone at place.org
Thu Oct 24 08:30:56 PDT 2013

This could be a "bug" in Hindley-Milner itself or its particular implementation in Haskell.  Depending on which formulations of set theory and term unification are used, the Axiom of Choice may indeed be axiomatic or derived.  Martin-Löf type theory does not entail that AoC --> LEM, but depending on details, this could have crept in...

Tl;dr:  retraction tentative, more investigation needed but I'm not going to do it now,  too busy fiddling with delimited continuations. ;-)

Chilly here in Stockholm but was warmer here at 20:00 last night than NY or Seattle at the same time.



On Oct 24, 2013, at 16:26, Jeff Bone <jbone at place.org> wrote:

> I should like to retract my previous long-standing objections to the Law of the Excluded Middle.
>   http://okmij.org/ftp/Computation/lem.html
> jb

More information about the FoRK mailing list