Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
32 lines (24 sloc) 857 Bytes
module Prelude.Functor
import Builtins
import Prelude.Basics
%access public export
||| Functors allow a uniform action over a parameterised type.
||| @ f a parameterised type
interface Functor (f : Type -> Type) where
||| Apply a function across everything of type 'a' in a
||| parameterised type
||| @ f the parameterised type
||| @ func the function to apply
map : (func : a -> b) -> f a -> f b
infixr 4 <$>
||| An infix alias for `map`, applying a function across everything of
||| type 'a' in a parameterised type
||| @ f the parameterised type
||| @ func the function to apply
(<$>) : Functor f => (func : a -> b) -> f a -> f b
func <$> x = map func x
||| Run something for effects, throwing away the return value
ignore : Functor f => f a -> f ()
ignore x = map (const ()) x
Functor (Pair a) where
map f (x, y) = (x, f y)
You can’t perform that action at this time.