Dougal Maclaurin

I'd be in favor of that. I think the reason I went with `{}` rather than `` initially was that `` looks strange when you write a function's type, because...

A simple version of this wouldn't be too hard to implement. I'm particularly thinking about the case where you only refer to previous methods within the same class (according to...

An alternative would be to have three different functions, like Haskell: ``` def putString (s:String) : {State World} Unit = ... def print (_:Show a) ?=> (x:a) : {State World}...

Specifically, quoting #1138 : 1. instances must be parametric over all data arguments. You can't define an instance like Ix (Fin 10). It has to be {n:Nat} (Ix (Fin n))...

Oh, that's definitely allowed! In your example, the function is an argument to the data constructor, `MkPoissonProcess`, rather than the type constructor, `PoissonProcess`.

If the hash is the performance bottleneck, should we use a cheaper one instead of the PRNG-grade threefry?

Thanks for the bug! This looks like an unintended consequence of the recent change that added implicit quantification (https://github.com/google-research/dex-lang/pull/699). One fix would be to avoid interleaving the `Ix n` constraints...

Yes, we don't have either recursive functions or recursive ADTs yet. It was a deliberate choice to de-prioritize them. They're fundamental to traditional functional programming, but Dex emphasizes arrays and...