m :: forall b. (? -> b) -> b
m x = x x
I don’t think you’d ever need such a function since PS supports recursion. I was just learning about Curry’s paradox and the fix-point combinator λf.(λx.xx)(λx.f(xx)). It made we wonder where the interplay with PS’s type system is.
My feeling is that you can’t do this sort of self-application. You use recursion as provided, but it doesn’t appear in the types.
I’ll have to play with it a bit. It looks like it’s actually the fixed-point combinator (which would make sense of the name)
Though the where clause is introducing recursion instead of self application. Still, that gives me ideas! Thanks for the link, no idea that existed 
The signature of fix seems strange to me, but I think I’ll need to play with it in the repl a bit later to follow.
This term is famously not typeable with rank-one types, but you can give it a few higher-rank typings, depending on how you intend to use it. Here’s one:
m :: forall f a. (forall b. b -> f b) -> f (a -> f a)
m x = x x
(Note that it is a general fact of higher-rank type systems that a unique most general higher-rank type for a term doesn’t necessarily exist.)
I didn’t realize it was famously so, but I did roughly get that impression.
I’ve had some trouble groking higher rank types in the past, but now that I think I really get what m is about, this is a good opportunity to dig into what’s happening here.
Thanks!
I’m getting this feeling like rank 2, forall can encorde a rank 1 exists? That that thought make sense? I may need some time to sort put my thoughts. Very nice though.
Earlier I’d written something like this:
type Λbool = forall a. a -> a -> a
λtrue :: Λbool
λtrue x _ = x
λfalse :: Λbool
λfalse _ y = y
λnot :: Λbool -> Λbool
λnot p = p λfalse λtrue
λand :: Λbool -> Λbool -> Λbool
λand p q = p q p
λor :: Λbool -> Λbool -> Λbool
λor p q = p p q
λimplies :: Λbool -> Λbool -> Λbool
λimplies p q = p q λtrue
λiff :: Λbool -> Λbool -> Λbool
λiff p q = p q $ λnot p
Which all worked as expected.
What I hadn’t realized then is that in this case, it seems like sometimes Λbool is rank 2 and sometimes it’s not. Should I be able to type this style of propositional logic semantics using rank 1 types? Not the way I’ve done it above, I suppose. Hmmm.
Λbool is a rank-one type, full stop. All the above types that use Λbool to the left of an arrow are rank-two types, by definition.
Λbool is rank 1
λnot is rank 2
Makes sense. Hmmm, alright.
I think λnot needs to be rank 2 in this case.
Terms don’t have ranks.
terms have types and types have ranks? It’s too generous to shorthand that terms have ranks?
I guess to your point that a term may have multiple types. Fair enough.
Exactly. Even without giving up principal types, many terms can be given a type having almost arbitrary rank.
The humble \x -> x, for example, has a principal type of forall a. a -> a, which is rank-one. But you could also give it a rank-zero type like Int -> Int, or a rank-two type like (forall a. a -> a) -> (forall b. b -> b), or in fact a type of arbitrarily high rank.
And that’s before anything even gets confusing.
This is very cool. Thank you. =)
I suppose what I meant is that if I gave Λbool a rank-0 type, then λnot wouldn’t compile as writ anymore. Though I’m not even sure that’s actually true. I think I’m officially confusing myself again! Okay. Well, good. motivation to learn!
I’m gonna toy around with this some more =)