Skip to content

Instantly share code, notes, and snippets.

@jcoglan

jcoglan/turing_types.md

Created July 4, 2014 18:12
Show Gist options
  • Save jcoglan/09076191352cf8d787e4 to your computer and use it in GitHub Desktop.
Save jcoglan/09076191352cf8d787e4 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
turing_types.md

Turing complete type systems

I'm trying to understand the computational power of different compiler components.

For example, JavaScript programs are Turing-complete, but recognising valid JS syntax only requires a CFG, not a Turing machine. The syntax is decidable, the semantics is not.

When people say 'Turing-complete type system', do they mean that user programs can use types to implement a Turing machine, or do they mean that the type checker is a Turing machine, or both?

If the latter, what is the purpose of such a type system? What is the value in having the system that checks the consistency/safety of programs itself be capable of running arbitrary programs?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment