News for hackers. Stuff that matters.
Re:The Y Combinator by bidirectional on Tuesday June 29, 2021 @11:28AM (#27677257)
Can you type that in System F? It doesn't seem logically valid, a -> a is trivially true, but apparently implies any a?
Re:The Y Combinator by scapp on Tuesday June 29, 2021 @01:25PM (#27678993)
System F isn't consistent as a logic (pretty much precisely because it has general recursion). In languages with general recursion, you can do things like

(Haskell)

    anyType :: a
    anyType = anyType
or

(Rust)

    fn any_type<T>() -> T {
        any_type()
    }
Re:The Y Combinator by gsg on Wednesday June 30, 2021 @12:23AM (#27684839)
System F doesn't have general recursion.

Extensions with a letrec-like construct are common, and are sometimes inaccurately called 'System F', but those languages do not have the properties of System F.

Re:The Y Combinator by scapp on Wednesday June 30, 2021 @07:00AM (#27687105)
You're right. I must have been thinking of one of those extensions you're talking about (F# maybe?). I should have remembered that System F is part of the lambda cube, so it's at least as consistent as CoC