Are there dependent type theories where not only are types values, but all values are (possibly singleton) types?
-
-
Replying to @milessabin
@TimSweeneyEpic's Lambda Aleph is in that direction http://www.leafpetersen.com/leaf/publications/dtp2013/lambda-aleph-overview.pdf …1 reply 0 retweets 2 likes -
Replying to @glaebhoerl @TimSweeneyEpic
That looks interesting ... thanks!
1 reply 0 retweets 1 like
Replying to @milessabin @glaebhoerl
McAllester's papers on Ontic (https://engineering.purdue.edu/~givan/papers/ontic-manual.pdf …) provide the cleanest exposition of types-as-sets-of-multiple-values.
3:15 PM - 12 Apr 2017
0 replies
0 retweets
2 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.