Polymorphic iteration/recursion

[AZMCode]

Hi! Newbie here!

First and foremost, love the language! Love the idea of a language that rules out deadlocks and is massively parallel.

I have been trying out things in the playground, primarily wanted to recreate Contexts from another research language I like, Koka.

Essentially a Context is a value with a hole in it, and you can iteratively refine the hole until you can fill it completely and obtain a finished value.

This is useful to abstract away and optimize iteration through lists, for example, to build a value "from the inside", to avoid reversing the list when you're done.

Now while this can be implemented natively, I just wanted to recreate the functionality in par for funsies.

Now, the type of this hole can change over each iteration, so with that context out of the way, this is the type I tried to express, in pseudo-par.

type Context = iterative [type a] [type hole] choice {
  . refine => [type newHole] [[newHole] hole] self(a,newHole)
  .fill => [hole] a
}

Thus a process on the other side of the Context would take the final fill, and apply the obtained functions in reverse order to get the filled out value.

Now, this is invalid code. In particular, this application of types to a self appears to be invalid.

I was wondering, is there a way to do these "polymorphic iterative types"?

Would this or equivalent functionality be considered for addition?

[faiface]

Hey! I'm happy you like the language! And fun stuff you're trying in it :D

This has actually come up and I've spent some time thinking about how to add it. It has a bunch of potential use-cases.

The syntax that you used in your post unfortunately couldn't work, that's because [type a] [type hole] ... is a type of values, it's not a type function, so you can't just apply it get a new type. It's just a concrete type of concrete values.

Here's a syntax that I was envisioning:

type Context<a, hole> = iterative<h = hole> choice {
  .refine => [type g] [[g] h] self<g>,
  .fill => [h] a,
}

The a doesn't need to go around since it doesn't change. The iterative<h = hole> would make the polymorphic iterative type and take hole as the initial assignment for h.

I'd love to see this feature in the language, as it has more use-cases. But I also wonder how it would affect subtyping checking, it would definitely complicate it, but I wonder how much.

[AZMCode]

Oh wow, that's a pleasant surprise! Yeah, sadly I don't know enough about compilers to help answer that question, but glad to see this is being considered. As per my intuition, this feels a bit GADT-y, so it might make the compiler/type inference significantly more complicated.

[NoamDev]

Just to clarify my understanding, the idea of context is actually already present in Par, right?

Using chan, and construction by destruction for example.