[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