idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-01 09:49:24 +03:00
Code Issues Projects Releases Wiki Activity

Add named instances for functor & applicative composition

Browse Source
This commit is contained in:
russoul 2021-02-10 20:05:32 +03:00 committed by André Videla
parent a060dcc18e
commit 1d23c7a6bd
1 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
libs/prelude/Prelude/Interfaces.idr
View File

@ -105,6 +105,12 @@ public export
ignore : Functor f => f a -> f ()
ignore = map (const ())
namespace Functor
||| Composition of functors is a functor.
export
[Compose] (Functor f, Functor g) => Functor (f . g) where
map fun = map (map fun)
||| Bifunctors
||| @f The action of the Bifunctor on pairs of objects
public export
@ -157,6 +163,15 @@ a *> b = map (const id) a <*> b
%allow_overloads (<*)
%allow_overloads (*>)
namespace Applicative
||| Composition of applicative functors is an applicative functor.
export
[Compose] (Applicative f, Applicative g) => Applicative (f . g)
using Functor.Compose where
pure = pure . pure
fun <*> x = ((<*>) <$> fun <*> x)
public export
interface Applicative f => Alternative f where
empty : f a