Composition of Closed Universes

[MaxDaten]

HI,

is it already possible but undiscovered by me to compose closed universes? For example: I want to share some elements (including semantics) between universes. For me this seems only achievable with nested records. This could be a bit too fiddling with a multi-level nesting. Any workarounds or ideas for composition of closed universes to form new closed universes?

[jonsterling]

Wow, that's a really good question! Basically, what you want is a union operator for these universes (a real union, not a sum)...

I don't presently know how to do that, but it would be truly wonderful if someone could figure it out! This would be a massive gain in modularity. I don't have a solution for you right now, but I want to keep this issue open—either we'll come up with something clever, or perhaps in the next formulation Vinyl we can take this very seriously as a requirement.

[MaxDaten]

Wow, that's a really good question!

Thanks :)

Basically, what you want is a union operator for these universes (a real union, not a sum)...

yes exactly. I'm currently studying your TH-Magic for these universes and semantics. But I'm really far away from being a TH expert. However I think an union for universes could be solved on TH level, because of the static nature of the current universe implementation. Or do I miss something?

But I'm without a concrete idea at the moment, too.

[jonsterling]

@MaxDaten It might indeed be possible to partially alleviate the problem with TH (though I'm not very good at it either, so I could be wrong)—though I suspect that the result would not be very compositional. But if you come up with any TH tricks to help with this, we'd be happy to take a look at them! :)