1.5 KiB
interpretation of sappho
Different aspects of sappho interpreted.
What is true?
Our "set interpretation" of types says true represents the full universe of
"things".
What are these things?
For all intents and purposes, a programmer can look at them as the values of our language.
What does this mean in practical terms?
Well, it means something of type true is "a value".
What is "a value" then?
That's a good question. It can be anything really.
An integer?
Yep!
A function?
Yes, m'am!
A solution to the halting problem?
Well, yeah! But good luck constructing that.
A...
I think you get my point. A value can be anything from a simple integer to nuclear apocalypse. The thing is, from the point of view of our program, it means "we cannot really say anything here".
But couldn't that be dangerous?
Depends on what you mean by dangerous.
I mean, to be able to give everything a type?
Well, let me ask you this: do you like rat poison?
What? To eat?
Yeah!
Nooo, that'd be dangerous!
Yeah, exactly my point.
What?
You know what rat poison is obviously, despite it being dangerous?
Well, yeah...
Maybe you got it already, but my point is: rat poison is dangerous, but you still know about it, and its existance. So, something being dangerous does not mean you have this blank spot of knowledge that you just keep ignoring because of this perceived danger.
interpretation of ⊢
what is the interpretation of
γ ⊢ δ?
given a concrete type k
conjunction of γ hold for k
then
disjunction of δ hold for k