Hacker News Reader

Comment by man-and-laptop | Hacker News Reader

Subtraction:

   let pred = λ(n : Natural) → (Natural/fold n { prev : Natural, next : Natural } (λ(p : { prev : Natural, next : Natural }) → { prev : p.next, next : p.next + +1}) { prev : 0, next : 0 }).prev 
   in λ(x : Natural) → λ(y : Natural) → Natural/fold y Natural pred x

The Ackermann function:

   let iter = λ(f : Natural → Natural) → λ(n : Natural) → Natural/fold n Natural f (f (1)) 
   in λ(m : Natural) → Natural/fold m (Natural → Natural) iter (+ +1)

Save the above to 'ack' and run the following: $ dhall <<< './ack 10 10' It's going to take a while before it finishes.

This language is close to Turing complete.

View on HN

Wait, so you can write programs in this thing that aren't primitive recursive? That's quite interesting; requiring primitive recursiveness is the usual way to guarantee termination. What class of programs does this language allow you to write? (It of course can't allow all programs that terminate, unless it also allows some that don't, which it claims not to.)

The type system appears to be System Fω[1], the “higher-order polymorphic lambda calculus”. I’m not really familiar with what class of programs it accepts, other than “more than simply typed lambda calculus”, but typechecking is decidable and evaluation is strongly normalising (i.e. both always terminate).

[1]: https://en.wikipedia.org/wiki/System_F#System_F.CF.89

Can somebody comment on what is missing for System F(ω) to be Turing complete?

I recall that it can typecheck self-application, so is it not possible to define and use the fixed-point combinator?

System Fw cannot type-check self application

The type system is what prevents System Fw from being Turing complete. Specifically, the key bit is that you cannot unify the type "a -> b" with "a" (which is what prevents self application)

System F can check self-application with an explicit type annotation, something like λx:(∀a. a → a). x [∀a. a → a] x, but Fω can’t.

I thought Fω was an extension of System F with type operators, so I figured if System F can check self-application, System Fω can too.

Am I missing something else?

Sorry, that comment was worded badly. Both System F and System Fω can express self-application at a particular type, but they can’t give a general type for self-application, e.g., Ω = ω ω where ω = λx.xx.

I see, thanks for the precision!

It's only guaranteed to terminate. That doesn't mean it's guaranteed to terminate before the heat death of the universe.

Can you limit evaluation to N reductions?

Author here: you could in principle, but in practice neither the library nor the executable compiler provide out-of-the-box support for limiting the number of reductions

Dhall's basic approach to safety is:

* make it impossible to intentionally do something malicious (such as destroying something important)

* make it hard to unintentionally do something incorrect or inconvenient (such as running for a long time)

For example, you can intentionally write a program that takes a very long time to run if you want to, but you will almost certainly know you are doing so; it's hard to write such a program by accident. In general, programming in a non-Turing-complete language forces you to structure code in such a way that potentially long-running code is more "obvious" than in Turing-complete languages.

Perhaps I should've added a :P to the end of that. See Gabriel's response here: https://news.ycombinator.com/item?id=15187733

For what is worth, Dhall lets you check if an expression is already in normal form: http://hackage.haskell.org/package/dhall-1.6.0/docs/Dhall-Co... so one could use Dhall as a "data-only" language without bothering with evaluation.

Yes? Do you foresee this being a typical thing to write in configuration files?

If we're being pedantic, as you were in your comment, "close to Turing complete" is not really a very precise term, is it?

When you have an issue, at least be explicit about it rather than just snarky. (See also Gabriel's other comments in this thread; not that I know or have any affiliation with him.)

Reply on news.ycombinator.com