3. So, I'm wondering if its possible to extend the HM type system to handle non-determinism in a similar fashion by either (i) having some function types be non-deterministic and/or (ii) having term types be non-deterministic. Taking the second approach, I suggest tagging each type with level [D] (for deterministic) or [N] (for non-deterministic). Notation-wise, if a determinism level is unspecified, then this means (I think) quantifying over determinism levels. A function that samples from the normal distribution we would get a type like:
normal:: double -> double -> () -> double[N]
Keep in mind that I don't know the first thing about type systems. I just babble about what feels right. With this said, this sounds like a completely new kind of term to me. Any by "kind", I mean as in "k" or "*". So some of the original examples could look like {-# LANGUAGE KindSignatures, NonDeterminism #-} normal :: Double -> Double -> () -> Double :: n sample :: (() -> a :: n) -> a :: n iid :: Int -> (() -> a :: n) -> [a :: n] constN :: (a :: *) -> (b :: n) -> (a :: *) -- also this: non-deterministic argument, but deterministic result where "n" is a new kind annotation replacing the [N] and the implicit "*" replaces the [D]. So the rules would have to be on the kind-level I suppose? Cheers.