Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- module Optic.Prism
- import Data.List
- %default total
- -- Const
- data Const a b = Constant a
- implementation Functor (Const a) where
- map _ (Constant x) = (Constant x)
- implementation Monoid m => Applicative (Const m) where
- pure _ = Constant neutral
- (Constant x) <*> (Constant y) = Constant (x <+> y)
- runConst : Const a b -> a
- runConst (Constant x) = x
- -- Prism
- Prism : Type -> Type -> Type -> Type -> Type
- Prism s t a b = {f : Type -> Type} -> Applicative f => (a -> f b) -> s -> f t
- prism : (a -> s) -> (s -> Maybe a) -> Prism s s a a
- prism encode decode fn s =
- case (decode s) of
- Nothing => pure s
- (Just v) => map encode $ fn v
- view : Prism s s a a -> s -> Maybe a
- view p x = runConst $ p (Constant . Just) x
- -- Maybe Prism
- justPrism : Prism (Maybe a) (Maybe a) a a
- justPrism = prism Just id
- getNat : Maybe Nat
- getNat = view justPrism (Just 1) -- Can't find applicative of f1.
Add Comment
Please, Sign In to add comment