[Haskell-cafe] Non-deterministic function/expression types in Haskell?
MarLinn
monkleyon at gmail.com
Thu Jan 11 22:18:08 UTC 2018
> 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.
More information about the Haskell-Cafe
mailing list