5 ms·

Subtraction: let pred = λ(n : Natural) → (Natural/fold n { prev : Natural, next : Natural } (λ(p : { prev : Natural, next : Natural }) → { prev : p.next, ne

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.

lomnakkus 9y ago
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.)
man-and-laptop 9y ago
Perhaps I should've added a :P to the end of that. See Gabriel's response here: https://news.ycombinator.com/item?id=15187733 https://news.ycombinator.com/item?id=15187733
imtringued 9y ago
It's only guaranteed to terminate. That doesn't mean it's guaranteed to terminate before the heat death of the universe.
- networked 9y ago
  Can you limit evaluation to N reductions?
  - Gabriel439 9y ago
    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.
ameliaquining 9y ago
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.)
- evincarofautumn 9y ago
  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 https://en.wikipedia.org/wiki/System_F#System_F.CF.89
  - chombier 9y ago
    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?
    - Gabriel439 9y ago
      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)
    - evincarofautumn 9y ago
      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.
      - chombier 9y ago
danidiaz 9y ago
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-Core.html#v:isNormalized 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.
- deleted 9y ago
  [deleted]

lomnakkus 9y ago

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.)

man-and-laptop 9y ago

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

imtringued 9y ago

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

networked 9y ago
Can you limit evaluation to N reductions?
- Gabriel439 9y ago
  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.

ameliaquining 9y ago

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.)

evincarofautumn 9y ago
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 https://en.wikipedia.org/wiki/System_F#System_F.CF.89
- chombier 9y ago
  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?
  - Gabriel439 9y ago
    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)
  - evincarofautumn 9y ago
    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.
    - chombier 9y ago

danidiaz 9y ago

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-Core.html#v:isNormalized 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.

deleted 9y ago
[deleted]