Right, but the type system is the constraint. Nobody's gonna take the untyped lambda calculus and run it on an accelerator. Even something like turing-completen

Right, but the type system is the constraint. Nobody's gonna take the untyped lambda calculus and run it on an accelerator. Even something like turing-completeness can be a type annotation, for example, the totality effect provided by languages like Koka.