packages feed

idris-0.9.9: lib/Control/Monad/Identity.idr

module Control.Monad.Identity

import Prelude.Functor
import Prelude.Applicative
import Prelude.Monad 

public record Identity : Type -> Type where
    Id : (runIdentity : a) -> Identity a

instance Functor Identity where
    map fn (Id a) = Id (fn a)

instance Applicative Identity where
    pure x = Id x
    
    (Id f) <$> (Id g) = Id (f g)

instance Monad Identity where
    (Id x) >>= k = k x