totality checking in nickel

[SomeGuyNamedMay]

does nickel plan on ever supporting totality checking to any degree? because some of my worst experences with nix were debuging recursive functions

[yannham]

Out of curiosity, were those recursive functions related to NixOS modules, or just plain recursive functions? Were there functions you wrote yourself, or that you consumed as part of a library?

For now, I must say that there's no such plan. Nickel is gradually typed and intentionally Turing-complete, which makes totality checking a bit of a challenge. The design philosophy here is to provide as many array and record combinators that you can do without recursive functions as much as possible. So, if you really want to avoid recursion, I think that should be possible, by just relying on std.array.xxx and std.record.xxx to iterate over/transform data structures. However, some tasks (typically traversing a heterogeneous JSON object to transform it) are really clumsy - if not impossible - without general recursion.

One angle we thought of, at some point, was to check totality for records. Because records are recursive by default, you could theoretically have loops there. But in practice what you want most of the time is a well-defined dependency tree (or DAG). This could be implemented without a lot of effort, as Nickel tracks (syntactically) the dependencies of record fields already.

[SomeGuyNamedMay]

just plain old recursive functions, I am curious, is there some property of gradually typed languages that make totality checking difficult? Ive never really gone to take a look at how proof assistants do it internally so i wouldn't know.

[yannham]

Well, the relevant part is not gradual typing per se but the presence of an untyped fragment (dynamically typed code). Without static types, you can encode fixpoint combinators, and thus recursion, without resorting to let rec or any other trickery:

nickel> let ycombinator = fun f => (fun x => f (x x)) (fun x => f (x x)) in
let factorial = fun recursive_call number => if number == 0 then 1 else number * (recursive_call (number - 1)) in
ycombinator factorial 5

120

I think this is kinda hard to rule out. This just makes use of higher-order functions and function application. In a typed language, you can rule this out easily if you want to, because the auto-application x x requires the type of x to satisfy the equation T ~= T -> T, which unless you have fancy recursive types, isn't true of simple types. Typically, the simply typed lambda calculus is an easy discipline for a functional language which ensures termination.

Usually proof assistants start from a known terminating and fully-typed fragment, from which they might add more powerful features, but with restrictions to always ensure termination. For example Coq has recursive functions but they must obey a simple syntactic criterion which ensures termination. I suspect this approach doesn't work so well when you don't have a statically typed language as a foundation to build upon.

That being said, the fixpoint example is a bit convoluted: if your goal is not to be exactly correct, but to rule out most of unintentional recursion, then there might be a simple criterion which works OK.
Another solution would be to require everything to be statically typed when checking for termination (you might end up in a fragment that resembles more Dhall, albeit with a different type system).

[SomeGuyNamedMay]

if you dont mind me asking what do you mean by recursive types? the wiki page seems two indicate that is just a shorthand for inductive types, which pretty much every proof assistent i can think of off the top of my head, including coq, supports.

[yannham]

"fancy" is a bit exaggerated, sorry for the confusion. I was thinking of so-called equirecursive types, but with a bit more boilerplate, you can in fact typecheck a fixpoint combinator with a simple inductive type e.g. in OCaml. I'm going to try to type the simplest loop possible, omega := (fun x => x x) (fun x => x x). Once again, x must have a type which satisfies (in some sense) an equation like T ~= T -> T. You can do that using a simple inductive algebraic datatype:

type iota = Roll of (iota -> iota)
(fun x -> match x with Roll x_unrolled -> x_unrolled x) (Roll (fun x -> match x with Roll x_unrolled -> x_unrolled x))

This typecheck and loops in OCaml (tested with v4.14.1). If you try to write this in Coq, Coq doesn't even let you write such an inductive type to begin with:

Inductive iota : Set :=
| unroll : (iota -> iota) -> iota.

gives

Non strictly positive occurrence of "iota" in "(iota -> iota) -> iota".

Coq forbids you from writing those kind of "cyclic" types as well. Then, Coq lets you write inductive types such as the list type, but you can still write a looping function there, so it has this additional guard restriction to forbid you from writing such looping functions as well.

[SomeGuyNamedMay]

that all makes sense, thanks for the information! im fairly new to plt so the information is appreciated.