88 lines
1.5 KiB
Markdown
88 lines
1.5 KiB
Markdown
# 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
|
||
|
||
|
||
|
||
|