Well then, let's at least make it formal.
Conversation
I think "is there a type for _terms_ of the embedded language" is the formal distinction I'd start with.
6
8
Yeah, that's how I understand it as well. It seems like a clear and useful distinction to me, and while I don't care for the deep/shallow terminology either, it doesn't seem any worse than other questionable terms, like Church/Curry for example.
2
7
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
I don't hate it, but like deep/shallow it does require you to look it up before you have any idea what it means.
1
2
deep/shallow at least you can learn what they mean.
1
2
wasn't church style where types can affect dynamic semantics and curry style is where they can't? or was it the other way around?
2
1
John Reynolds called Curry typing "extrinsic" and Church typing "intrinsic". Extrinsic semantics assigns meaning to phrases, whereas the intrinsic one assigns it to judgements. See cs.cmu.edu/afs/cs/user/jc
1
1
8
I VASTLY prefer extrinsic/intrinsic to curry/church.
3
12
I always somehow mix up extrinsic/intrinsic with extensional/intensional. Maybe it's because they start with the same letters? Still not sure I have my head around difference! 😅
2
1
Not saying that as a criticism of the terminology (extrinsic/intrinsic does seem much better than curry/church), more just my own silly brain doing silly things as I learn this stuff!