Trying to bend my head around the language

[tobega]

I see that Nat.Repeat is a recursive either, but if I try to create, say, a Countdown that is consumed as a recursive either, how do I do that?

Creating recursive either instances seems only to be able to be done explicitly, while making something that loops on a condition seems to have to be a choice.

Is this where I have to create a dual type, a Downcounter as an iterative choice, which gets exposed by the channel? Or actually, it becomes dual automatically?

[faiface]

Hi and welcome! I'll be more than happy to help you, however I'm not really understanding what you mean. Could you expand and/or perhaps provide code examples in another language (or what you attempted in Par) to make it clearer what you'd like to accomplish?

[tobega]

I can simplify: How would I implement Nat.Repeat in par-lang itself?

As for the other musings, I'm starting to suspect that there is a lot of syntax sugar that makes it harder for me to understand at this stage. My dawning understanding is that creating a value is actually working on the dual of that value's type.

[faiface]

How would I implement Nat.Repeat in par-lang itself?

The simplest, but incomplete answer to that is that you would not. It is possible by using .unfounded, the escape hatch that enables non-well-founded recursion, but without it it's impossible.

That's intentional. In Par, recursion and looping are meant to be always terminating and the mechanism chosen to accomplish this is the recursive (and iterative) types. The recursive types are guaranteed to be finite, and so looping on them is fine.

But, for the purposes of efficiency, Nat is not a recursive type by itself. It has an efficient byte representation, and efficient arithmetic operations via Nat.Add, Nat.Mul, etc. functions. The Nat.Repeat built-in function is exactly what says: you can loop on this. It is what enables the recursion on Nats. This kind of a thinking is true for all primitive types. On their own, they're opaque, but the functions that come with them give them their abilities.

However, let me show you how you could implement Nat.Repeat using .unfounded. At this point, .unfounded is still required to loop on a recursive, which is a little unfortuante (we'll need to change that to enable looping on anything), so we'll have to construct a useless recursive value to loop on. Here's how it can look:

dec MyRepeat : [Nat] recursive either {
  .end!,
  .step self,
}

def Driver : recursive ! = !  // fake recursive

def MyRepeat = [number]
  do { Driver.unfounded } in Nat.Equals(number, 0).case {
    .true! => .end!,
    .false! => let number = Nat.Max(0, Int.Sub(number, 1)) in .step Driver.loop,
  }

[faiface]

My dawning understanding is that creating a value is actually working on the dual of that value's type.

Yep, that's actually right :) You can quite reasonably see Par's values as being channels "to the other side", where the other side is some process operating on the dual.

[tobega]

This confuses me a little, though, because there is no problem creating an infinite stream.

I could create a static value instance of MyRepeat by just calling .step.step.step.end right?

So in construction of the value I am actualling working on an iterative choice (the dual). It seems to me I should be able to loop on that?

[NoamDev]

Looping on a possibly infinite stream could possibly never finish.
Par aims to be total, so it doesn't let you do that. You only loop on recursives whose defining trait is that looping them is guaranteed to finish at some point.