[Nix-dev] with, ++, //, and laziness

[Nicolas Pierron]

Hi,

On Sun, Mar 25, 2012 at 20:18, Shea Levy <shea at shealevy.com> wrote:
> On 03/25/2012 12:38 AM, Nicolas Pierron wrote:
>>
>> rec {
>>   a = with<ATTRNAMES>;<LAZY>  { c = 1; d =<LAZY>  c; };
>>   b =<LAZY>  a //<LAZY>  { c = 2; };
>> }
>> in b.d
>> oul
>>
>> <ATTRNAMES>  implies that we need to be able to iterate over the "with"
>> clause attribute set to bind names such as "c".
>
>
> Even accepting that for 'with b; { c = 1; d = c }' we have to be able to
> know that b is an attribute set and get all the attribute names for b, I
> still don't see why this should be an infinite recursion. We know all the
> attribute names for 'with b; { c = 1; d = c }': c and d (no matter what b
> is, the attribute names are c and d). Similarly, the attribute names for { c
> = 2 } are just c. So we know all the attribute names for b: c and d. Where
> does the infinite recursion come in?

Trust me, this the biggest issue in NixOS and I already ask Eelco
multiple times about it.
The problem is that knowing the signature such as int, string,
attribute set of ["c" "d"] is not yet handled in the semantic of Nix
language.

One of the proposal I have for the Nix language semantic modification is:

typeOf null  == null
typeOf true  == false
typeOf false  == false
typeOf 5  == 0
typeOf "string" == ""
typeOf […] == [ ]
typeOf { a = …; b = …; } == { }
typeOf (x: …) == (x: true)

typeOf (a && b) == false
typeOf (a || b) == false
typeOf (a -> b) == false
typeOf (a + b) == ""
typeOf (a ++ b) == [ ]
typeOf (a // b) == { }
typeOf (if c then t else e) == if c then typeOf t else typeOf e
typeOf ((x: …) v) == (x: typeOf …) v
…

What you need is a bit more than typeOf because you need attrNames to
be an additional logic rule of the evaluation of Nix which correspond
to:

attrNames { } == [ ]
attrNames { b = …; a = …; } == ["a" "b"]
attrNames (a // b) == uniqList (mergeSort (attrNames a) (attrNames b))
attrNames (if c then t else e) == if c then attrNames t else attrNames e
attrNames ((x: …) v) == (x: attrNames …) v

Another way could be to provide introspection rules to collect these
information from Nix it-self.

The problem is that adding such rules implies that you need to handle
them in addition to the default Eval rule and is likely to increase
the complexity of future optimizations of the Nix language.

>> I think the behaviour
>> you expected was the case for the first versions of Nix where we had
>> maximal laziness for caching binding rules.<ATTRNAMES>  implies to
>> solve b and the "extend" operator.
>>
>
> What does 'solve b' mean here? Surely we don't have to evaluate each
> attribute of b, and I already showed that we can determine the attribute
> names of b without any infinite recursion.

solve mean matching the left-hand side and replacing it by the right
hand side in semantic rules such as:

Eval (a // b) == Attribute set with all attributes of (Eval b)
completed with non-overlapping set of attributes of (Eval a).

Having the "typeOf" rule will solve the strictness issue of NixOS,
having "AttrNames" can be used to remove __override special attribute
by changing the strictness with.
Eelco, what do you think ?

-- 
Nicolas Pierron
http://www.linkedin.com/in/nicolasbpierron - http://nbp.name/