Live data from Hacker News

Is Type Theory Turing Complete?

news.ycombinator.com

1–2 of 2 posts

Is Type Theory Turing Complete?

#1
I'm working with interval arithmetic.

Intervals have the annoying arithmetic behavior of tending to get wider. So [1..3]+[2..5] ends up with [1..8]

On the other hand, if I'm trying to compute the "cover" of an area this tendency to cover more area is what I want.

On the third hand, it seems that singleton intervals mirror arithmetic. So [1..1]+[2..2] ends up with [3..3]. Since I have addition it seems I get multiplication.

Which leads me to the question... is type theory turing complete? Can I compute any result using only types? Can I create a "type computer"?