Created
March 30, 2020 12:41
-
-
Save byzantic/8d23e97652ecd26e7c2916f083316549 to your computer and use it in GitHub Desktop.
Unison Monads
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- This gist shows how we can use abilities to provide nicer syntax for any monad. | |
| -- We can view abilities as "just" providing nicer syntax for working with the | |
| -- free monad. | |
| ability Monadic f where | |
| eval : f a -> a | |
| -- Here's a monad, encoded as a first-class value with | |
| -- two polymorphic functions, `pure` and `bind` | |
| type Monad f = Monad (forall a . a -> f a) (forall a b . f a -> (a -> f b) -> f b) | |
| use Monad Monad | |
| Monad.pure : Monad f -> a -> f a | |
| Monad.pure = cases Monad pure _ -> pure | |
| Monad.bind : Monad f -> f a -> (a -> f b) -> f b | |
| Monad.bind = cases Monad _ bind -> bind | |
| -- Just as we can interpret `Free f a` into `f a` given a monad | |
| -- for `f`, we can interpret a `'{Monadic f} a` into `f a` given | |
| -- a monad for `f`. | |
| -- | |
| do : Monad f -> '{Monadic f} a -> f a | |
| do m actions = match m with | |
| Monad pure bind -> | |
| go = cases | |
| {a} -> pure a | |
| {Monadic.eval fa -> k} -> bind fa (a -> handle k a with go) | |
| handle !actions with go | |
| use Optional | |
| optionalMonad : Monad Optional | |
| optionalMonad = | |
| bind : Optional a -> (a -> Optional b) -> Optional b | |
| bind oa f = match oa with | |
| None -> None | |
| Some a -> f a | |
| Monad Some bind | |
| > do optionalMonad 'let | |
| x = eval (Some 1) | |
| 1 + eval (Some 2) | |
| -- the above implentation taken from | |
| -- https://gist.github.com/aryairani/d561ffea4762499432b3ad3355313fe8 | |
| -- Actually, my main reason for exploring the Monad implementation here | |
| -- is to use it to implement Functors and Applicative Functors. | |
| -- this is not possible in general, but List and OPtional can serveas examples. | |
| -- First of all, then, lets implement the List Monad | |
| use List | |
| listMonad : Monad List | |
| listMonad = | |
| bind : List a -> (a -> List b) -> List b | |
| bind la f = match la with | |
| [] -> [] | |
| a +: as -> (f a) ++ (bind as f) | |
| Monad (x -> [x]) bind | |
| >do listMonad 'let | |
| x = Monadic.eval ([1]) | |
| 2 + Monadic.eval ([3]) | |
| -- this is a bit like a list comprehension | |
| >do listMonad 'let | |
| x = Monadic.eval ([1,2,3]) | |
| Monadic.eval ([x * x]) | |
| -- so lets try to generalise it | |
| listComp : (e -> g) -> List e -> List g | |
| listComp f l = do listMonad 'let | |
| x = Monadic.eval l | |
| Monadic.eval ([f x]) | |
| >listComp (n -> n Nat.* n) [1,2,3] | |
| >listComp (n -> n Nat.< 5) [1,2,3,4,5,6,7,8,9] | |
| -- well actually, its just 'map' | |
| >map (n -> n Nat.< 5) [1,2,3,4,5,6,7,8,9] | |
| -- try to generalise this over any Monad | |
| mapM : Monad f -> (e -> g) -> f e -> f g | |
| mapM m1 f v1 = do m1 'let | |
| x = Monadic.eval v1 | |
| Monadic.eval (Monad.pure m1 (f x)) | |
| >mapM listMonad (n -> n Nat.* n) [1,2,3] | |
| >mapM optionalMonad (n -> n Nat.* n) (Some 4) | |
| -- ok, but maybe we could just do that using Monad identities | |
| liftM : Monad m -> (a -> b) -> m a -> m b | |
| liftM m1 f ma = (Monad.bind m1 ) ma ((Monad.pure m1) . f) | |
| >liftM listMonad (n -> n Nat.* n) [1,2,3] | |
| >liftM optionalMonad (n -> n Nat.* n) (Some 4) | |
| -- ok, but what about List as a non-deterministic monad? | |
| -- the standard example is to choose pairs of values taken from lists | |
| -- | |
| choosePairs : List a -> List b -> List (a,b) | |
| choosePairs xs ys = do listMonad 'let | |
| a = Monadic.eval xs | |
| b = Monadic.eval ys | |
| (a,b) | |
| >choosePairs [1,2,3] [4,5,6] | |
| -- again we could generalise this to any monad | |
| zipMwith : Monad m -> (a -> b -> c) -> m a -> m b -> m c | |
| zipMwith m f m1 m2 = do m 'let | |
| a = Monadic.eval m1 | |
| b = Monadic.eval m2 | |
| f a b | |
| >zipMwith listMonad (a b -> (a,b)) [1,2,3] [4,5] | |
| -- since any Monad is also an Applicative, can we implement apply? | |
| -- granted, this is doing things backwards, but hey .. | |
| applyM : Monad m -> m (a -> b) -> m a -> m b | |
| applyM m mf ma = do m 'let | |
| f = Monadic.eval mf | |
| a = Monadic.eval ma | |
| f a | |
| -- so this should be the same as liftM | |
| fmapM : Monad m -> (a -> b) -> m a -> m b | |
| fmapM m f = applyM m ((Monad.pure m) f) | |
| >fmapM listMonad (n -> n Nat.* n) [1,2,3] | |
| -- TODO a better example of apply | |
| ---- | |
| I found and typechecked these definitions in | |
| /mnt/c/work/wsl/develop/tutorials/unison/abtut/monad.u. If you do an `add` or `update`, here's | |
| how your codebase would change: | |
| ⍟ These new definitions are ok to `add`: | |
| type Monad f | |
| ability Monadic f | |
| Monad.bind : Monad f -> f a -> (a -> f b) -> f b | |
| Monad.pure : Monad f -> a -> f a | |
| applyM : Monad m -> m (a -> b) -> m a -> m b | |
| choosePairs : [a] -> [b] -> [(a, b)] | |
| do : Monad f -> '{Monadic f} a -> f a | |
| fmapM : Monad m -> (a -> b) -> m a -> m b | |
| liftM : Monad m -> (a -> b) -> m a -> m b | |
| listComp : (e ->{Monadic List} g) -> [e] -> [g] | |
| listMonad : Monad List | |
| mmap : Monad f -> (e -> g) -> f e -> f g | |
| optionalMonad : Monad Optional | |
| zipMwith : Monad m -> (a -> b -> c) -> m a -> m b -> m c | |
| Now evaluating any watch expressions (lines starting with `>`)... Ctrl+C cancels. | |
| 42 | > do optionalMonad 'let | |
| ⧩ | |
| Some 3 | |
| 56 | >do listMonad 'let | |
| ⧩ | |
| [5] | |
| 61 | >do listMonad 'let | |
| ⧩ | |
| [1, 4, 9] | |
| 71 | >listComp (n -> n Nat.* n) [1,2,3] | |
| ⧩ | |
| [1, 4, 9] | |
| 72 | >listComp (n -> n Nat.< 5) [1,2,3,4,5,6,7,8,9] | |
| ⧩ | |
| [true, true, true, true, false, false, false, false, false] | |
| 75 | >map (n -> n Nat.< 5) [1,2,3,4,5,6,7,8,9] | |
| ⧩ | |
| [true, true, true, true, false, false, false, false, false] | |
| 83 | >mmap listMonad (n -> n Nat.* n) [1,2,3] | |
| ⧩ | |
| [1, 4, 9] | |
| 84 | >mmap optionalMonad (n -> n Nat.* n) (Some 4) | |
| ⧩ | |
| Some 16 | |
| 91 | >liftM listMonad (n -> n Nat.* n) [1,2,3] | |
| ⧩ | |
| [1, 4, 9] | |
| 92 | >liftM optionalMonad (n -> n Nat.* n) (Some 4) | |
| ⧩ | |
| Some 16 | |
| 103 | >choosePairs [1,2,3] [4,5,6] | |
| ⧩ | |
| [(1, 4), (1, 5), (1, 6), (2, 4), (2, 5), (2, 6), (3, 4), (3, 5), (3, 6)] | |
| 120 | >zipMwith listMonad (a b -> (a,b)) [1,2,3] [4,5] | |
| ⧩ | |
| [(1, 4), (1, 5), (2, 4), (2, 5), (3, 4), (3, 5)] | |
| 128 | >fmapM listMonad (n -> n Nat.* n) [1,2,3] | |
| ⧩ | |
| [1, 4, 9] |
Author
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This gist includes a copy of this gist, which shows a technique of implementing Monads in Unison.
The intent here is just to develop a few more examples of using the technique. The do function here does allow a very similar way of working with Monads compared to Haskell. I don't mind the need to supply a concrete Monad, as this does allow the use of different interpretations of the same data structure.
The use of the List Monad as a non-deterministic Monad drops out quite nicely here (see choosePairs), and can be compared to the 'Choose' ability defined in the Abilities tutorial.
Actually, my real interest is in how to get to the equivalent of Functors and Applicative Functors. I'm not so bothered about Monads per se, because they always seem to require a lot of 'plumbing' to work, and it looks as though Abilities could be a rather richer abstraction anyway. But I am worried about supporting Functors, because they are so useful, and it is very powerful to be able to use a polymorphic function with any Functor. In addition, it seems that many of the traditional uses of Monads can be performed using Applicative.
So the latter part of the gist is a cheat; if you have a Monad, it is (always?) an Applicative or Functor also, so we can derive a generic 'fmap' and 'apply'.
By the way, I should point out I'm not an expert at any of this, I'm highly likely to be mistaken about all sorts of things.