@CapitalEx OOOoooh, I think you're right. I hadn't made the connection with the halting problem, but that's true, I guess a specific type is indeed the solution here.
Top-level
@CapitalEx OOOoooh, I think you're right. I hadn't made the connection with the halting problem, but that's true, I guess a specific type is indeed the solution here. 4 comments
@CapitalEx I'm an absolute beginner when it comes to building type systems, so this is all fresh to me. I've been going through the handlful of papers and blog posts on types/concat languages. This morning @toxi gave me a bunch of very interesting links on the topic: https://merveilles.town/@toxi@mastodon.thi.ng/110362257067437570 I'll keep reporting my findings, I've started a stub on the topic here: http://wiki.xxiivv.com/site/type_systems.html @toxi @CapitalEx I promise I'll try to not get sucked in too deeply that I can never re-emerge. :moomin_hello: |
@neauoire :: (oops broke that one reply by accident)
Interested in what ideas you explore within Tal's limits. FP languages have the advantage of a strong type system and pattern matching. If your type is finite and each step reduces the given inputs to their base cases, you can say confidently that "this loop terminates".
Idris does this, but it also means some finite functions can't be statically resolved and are marked as partial.