4 ms·

Then of course there are monads which aren't too inappropriately described as the pattern of expressing controlled imperative features in the type system.

• tomp 12y ago
  The difference between monads and the kind of effects system used in Koka is that in Koka, effects are inferred, whereas with monads, they have to be stated up-front. Koka also allows you to mix effects, e.g. a function can be `<io, st<h>, ndet>`, meaning that it reads/writes files, reads/writes memory in heap `h`, and is non-deterministic. Effect variables are akin to higher-kinded polymorphism, so that e.g. `map` can be polymorphic in the effect of the mapping function.
  • aninhumer 12y ago
    >in Koka, effects are inferred Monadic types can be inferred most of the time in Haskell, it's just considered good practice to include a type signature for every function. >Koka also allows you to mix effects, e.g. a function can be `<io, st<h>, ndet>` This can be done with Monad transformers, although it's a little awkward at the moment. There are various proposals for better composition here, and I suspect sooner or later someone will work out a good solution. >`map` can be polymorphic in the effect of the mapping function. `mapM` is polymorphic over monadic functions. `map` doesn't handle monadic functions (unless you just want a list of monadic values), but since they're kind of different operations, I think it's preferable to have different functions for each.
  • freyrs3 12y ago
    mtl has been around for a while now and using any the monads from the mtl transformers library is very inferrable, although like any inference it returns the most general type possible and it's generally just good practice to forward declare the type. example = do a <- ask modify (+ a) b <- get tell [b] GHC correctly infers: example :: (Num s, MonadState s m, MonadReader s m, MonadWriter [s] m) => m ()
  • tel 12y ago
    As others have stated, that's all done as libraries in Haskell in a variety of ways. I'd be interested in knowing how the order of the combined effect types are resolved in Koka, though. For instance, in `<io, ndet>` the ndet effect will end up conducting a search. How do the (observable) io side effects get woven into that search? In particular, how does Koka know the proper ordering? In Haskell, you'd be forced to eventually declare an order to your monad stack (although most functions can be agnostic to the particular choice). So in this instance, you would write `LogicT IO a` to indicate that the non-determinism gets resolved first while most functions would be of the form `(MonadIO m, MonadLogic m) => m a` where the parenthesized set of constraints is unordered.
    • tomp 12y ago
      Hm... if I understand correctly, the `ndet` effect isn't non-determinism in the sense of amb, but rather non-determinism in the sense or random. I.e., there is no search, it's just producing a random number.
      • tel 12y ago
        Ah, sorry. The question still holds, though it's less obvious what it means with this effect stack. Perhaps a more obvious example would be failing, stateful computation written as follows as an order-free restricted type in Haskell ( MonadPlus , MonadState s ) => m a Given some concrete choices of monads to witness those effects like MaybeT and StateT there are two "orders" we can stack them. MaybeT (StateT s Identity) a StateT s (MaybeT Identity) a where Identity forms the "effect free" base of our stack. While functions which operate on types with the order-free signature work for each stack, ultimately the stacks represent different combined effects. In particular, the `StateT s (MaybeT Identity)` stack throws away state if the computation fails while `MaybeT (StateT s Identity)` does not. run1 :: StateT s (MaybeT Identity) a -> s -> Maybe (s, a) -- failure captures the result state run2 :: MaybeT (StateT s Identity) a -> s -> (s, Maybe a) -- result state always produced, failure captured -- only in the result value So, ultimately the semantics of your effect set depend upon the ordering of your effects. At least in Haskell. I'd be interested to see how Koka handles it.
• deleted 12y ago
  [deleted]
• dllthomas 12y ago
  On the topic of Lisp and monads, it occurred to me recently that Lisp "lists" are actually rose trees, and rose trees are a free monad. Which winds up being a more Haskelly take on "In Lisp, you're writing out the AST".