Nested definitions

[xsebek]

Feature

I would like to def inside def. It seems well defined in that def-end would nest properly and replace previous definitions.

Example

For example, if I wanted to avoid coming up with variable names for built robots, I could create a registry function:

def i = 0 end
def registry : int -> robot = \i. error "no such robot in registry" end

Building a registered robot is as easy as:

r <- build {}; def i'=i end; def i=i+1 end def r'=registry end; def registry=\j. if (j == i) {r} {r' i} end

Which would be nice to wrap in an outer definition:

def builder: {cmd a} -> cmd robot =  \cmd.
  r <- build cmd; def i'=i end; def i=i+1 end def r'=registry end; def registry=\j. if (j == i) {r} {r' i} end
end
// Definitions may only be at the top level: def i' = i end

Solution

I can imagine running a cmd could modify the outer definitions. The inner defs would need to be collected in infer and then put into the outer context when the outer def is called:

def i = 0 end
def f = def i = i + 1 end; end
// i is still 0
f
// i is now 1

Not sure if it would be necessary to store the outer def parameters somewhere so the inner defs could still access them.

I have a feeling this is Pandora's box with many nasty bugs that could occur when the inner context calls some forgotten variable, but it could be fun to have self-modifying programs. 😂

Alternatives

• Lists or maps (Recursive types #154) would be a cleaner way to store robots.
• Macro functions could do the job. 😈

[byorgey]

Hmm, I totally understand what you're trying to do here, and the example with making a registry is a nice example. However, I'm not sure that nested definitions is the way to accomplish this. Essentially it seems like you're trying to use variables created via def as if they are global, mutable variables, but they're really not. In particular, although you can shadow the definition of registry with a new definition, any previously defined things which refer to registry will still see the value it had at the time they were defined (even if their evaluation is delayed until later). Once you had registry being updated via builder, you might want to also encapsulate other functions that referred to registry, but this would not work, since they would never see any updates to it; you would only be able to use registry directly at the REPL.

I think the better way to accomplish this would be through the use of real mutable references, which would not be hard to add, given that we already use a CESK machine (I thought we already had an issue for that but perhaps not).

The reason we don't allow nested def is because... well, actually, I'm not sure I completely remember the reasons. It might have to do with making it easier to do capability inference (although that is still kind of broken anyway). If I remember more about why that choice was made I'll update this issue.

[xsebek]

Regarding the example, I think it is better for builder function to return a pair of current index and mapping:

def builder : (int * (int -> robot)) -> {cmd a} -> cmd (int * (int -> robot)) = \robM. \comm.
  r <- build comm;
  let i : int = fst robM in
  let m : int -> robot = snd robM in
  return (1+i, \j. if (j == i) {r} {m j});
end;

> def register : int -> robot = \i. error ("No registered robot with id " ++ format i) end;
> rM <- return (0, register);
(0, \i. error ("No registered robot with id " ++ format i)) : int * (int -> robot)
> rM <- builder rM {move; move};
(1, let i = 0 in let m = \i. error ("No registered robot with id " ++ format i) in let r = <r2> in \j. if (j == i) {r} {m j}) : int * (int -> robot)
> snd rM 0
<r2> : robot

I run into #333 trying to use the readable definition from a file and into #351 when I did not constrain the types. 🐛

But with some copy-pasting, it works! 🥳

^{I am missing devices required for '+' though...}

[xsebek]

Just to link it here, in #373 I encountered the following note in build step:

        -- Note that _capCtx must be empty: at least at the
        -- moment, definitions are only allowed at the top level,
        -- so there can't be any inside the argument to build.
        -- (Though perhaps there is an argument that this ought to
        -- be relaxed specifically in the case of 'Build'.
        let (caps, _capCtx) = requiredCaps (r ^. robotContext . defCaps) cmd

I wonder if that would be harder or simpler than nested definitions, but definitions in build and reprogram sound useful 🙂

But as it can be worked around, we can leave it for later.

[byorgey]

Although nested definitions wouldn't really help with the original motivation written here, nested definitions are still a sebsible idea. To allow them we would have to first implement #636 and possibly #231 .

[xsebek]

I no longer think this is useful - the original example can be implemented more cleanly in other ways.

A def inside build does not give any extra power than let, because once the robot stops, its definitions are no longer useful.