Should general recursion always be allowed?

[Invisible-Rabbit-Hunter]

It feels like general recursion could be problematic in some cases, such as defining a functor

ar Cat bad : Base --> Base = bad

Should this always be allowed?

[evincarofautumn]

Maybe recursion could impose the requirement that the target category is traced?

The desugaring of a hypothetical pointful notation (#9) could be the same as GHC’s desugaring of rec in its arrow notation.

[jameshaydon]

Great questions, this actually came up in my current work on moving the JS category/interpretation into Lawvere itself.

Yes, for the moment the system assumes that the category supports mutually recursive definitions of arrows, but this isn't ideal.

Should this always be allowed?

Probably not, and I'm open to suggestions on this. But my focus right now is in providing tools for programming in categories, and experimenting with what that programming paradigm looks like, rather than on making sure it's all safe. But it's still something I'd like to think about and implement at some point.

Maybe recursion could impose the requirement that the target category is traced?

Yes. The basic idea is that when one defines an arrow in Base (or doesn't specify the category at all), the system will just assume that the user is defining an arrow in the initial category with whatever features/effects the programmer uses, similar to how Haskell will infer type-classes being used, e.g. the ArrowLoop class in the case that rec is being used. However that still doesn't really tackle that each file still contains a bunch of possibly mutually recursive definitions in possibly multiple categories. So instead I think it should be something more like Idris:

A Lawvere file allows for:

• A sequence of definitions; each definition for a specific category.
• Each definition is only allowed to reference the definitions before it, or itself (if the category is traced),
• One can define multiple mutually recursive definitions in a single category using a new keyword mutual (or rec).

[Invisible-Rabbit-Hunter]

There are also recursion schemes, which seem quite relevant to this, I would assume.

[jameshaydon]

There are also recursion schemes

Indeed they are, and in fact recursion-schemes was the main reason I made Lawvere (and why it's called "Lawvere"), but then I got side-tracked into implementing effects. The way I want recursion schemes to work is explained here: https://github.com/jameshaydon/lawvere/blob/master/examples/presentation.law.md, where the example is a type of expressions for some language.

The general idea is that one defines sketches, models (functors) between the Lawvere theories of those sketches (that's why the language is called 'Lawvere'), and natural transformations between these models. But this part is really only being experimented on at the moment (and assumes all models are in Base), but this example works (though nothing is type-checked):

Define a sketch for lists of integers:

sketch ListSk over Base = {
  ob List,
  ar empty : {} --> List,
  ar cons  : { head: Int, tail: List} --> {}
}

Define a morphism in the theory generated by that sketch:

ar Base[ListSk] list123 : {} --> List =
  empty
  { head = ~3, tail = } cons
  { head = ~2, tail = } cons
  { head = ~1, tail = } cons

Define an interpretation of the theory back into Base, via interpreting the sketch:

ar Cart sum : Base[ListSk] --> Base =
  sketch_interp ListSk {
    ob List  |-> Int,
    ar empty |-> 0,
    ar cons  |-> .head + .tail
  }

One can then interpret morphisms of the theory directly:

ar Base six : {} --> Int = sum(list123)

(sum(list123) has type sum({}) --> sum(List), that is, {} --> Int)

Or alternatively, the theory comes with an initial model, and one can then use the natural transformation from the initial model into this model to get an arrow from_init(sum)(List) in Base:

ar Base : alsoSix : {} --> Int = init_interp(ListSk)(list123) from_init(sum)(List)

Here init_interp(ListSk) is this initial model Base[ListSk] --> Base; init_interp(ListSk)(List) is an object of base that represents lists of integers. And from_init(sum) is a natural transformation from this initial model into the sum model. At List, this produces an arrow in Base from init_interp(ListSk)(List) (i.e. lists of integers) to sum(List) = Int (which sums the list).