48 lines
1.1 KiB
Agda
48 lines
1.1 KiB
Agda
module Prelude
|
|
|
|
data Nat : U where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
data Maybe : U -> U where
|
|
Just : {a : U} -> a -> Maybe a
|
|
Nothing : {a : U} -> Maybe a
|
|
|
|
data Either : U -> U -> U where
|
|
Left : {a b : U} -> a -> Either a b
|
|
Right : {a b : U} -> b -> Either a b
|
|
|
|
-- TODO this is special cased in some languages, maybe for easier
|
|
-- inference? Figure out why.
|
|
|
|
infixr 0 _$_
|
|
|
|
-- Currently very noisy in generated code
|
|
_$_ : {a b : U} -> (a -> b) -> a -> b
|
|
f $ a = f a
|
|
|
|
|
|
-- Monad
|
|
|
|
-- TODO stack with Applicative, etc?
|
|
|
|
data Monad : (U -> U) -> U where
|
|
MkMonad : { M : U -> U } ->
|
|
(bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
|
|
(pure : {A : U} -> A -> M A) ->
|
|
Monad M
|
|
|
|
infixl 1 _>>=_ _>>_
|
|
_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
|
|
_>>=_ {a} {b} {m} {{MkMonad bind' _}} ma amb = bind' {a} {b} ma amb
|
|
|
|
_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
|
|
ma >> mb = mb
|
|
|
|
pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
|
|
pure {_} {_} {{MkMonad _ pure'}} a = pure' a
|
|
|
|
-- IO
|
|
|
|
|