2 ms·

Can you type that in System F? It doesn't seem logically valid, a -> a is trivially true, but apparently implies any a?

• scapp 5y ago
  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() }
  • gsg 5y ago
    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.
    • scapp 5y ago
      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