Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
There’s also a stub at parallel computing. Here’s an account of the difference. I wonder if there’s anything nPOV-ish to say.
I wonder if there’s anything nPOV-ish to say.
With computation understood as path lifting (here) parallel computing should correspond to the case that the base type over which we lift is itself further fibered, so that a single path (= instruction path = program) is itself the (dependent-)pairing of several other paths in spaces of subsets of the parameters.
That’s interesting. We’ve spoken before about when (what we now call) a type telescope doesn’t use the full range of dependencies, for instance, back here. There’s Mike’s concept of “context shape” in #27 there.
a type telescope doesn’t use the full range of dependencies
Not sure if that’s the right way to put it.(?) Subject to there being a linear ordering on the context extensions, type telescopes reflect the most general possible dependencies.
(The discussion you link to indeed starts with considering a type telescope and then considers specializing it to situations where some types up in the telescope do not explicitly depend on some of the previous stages.)
1 to 8 of 8