Granule documentation

Module Maybe

Meta-data

Description: Library for working with values that may be absent
Authors: Vilem-Benjamin Liepelt, Dominic Orchard
License: BSD3
Copyright: (c) Authors 2018
Issue-tracking: https://github.com/dorchard/granule/issues
Repository: https://github.com/dorchard/granule

data Maybe (a : Type) where
    Nothing 
  ; Just a

Type-safe null; wrap a computation that could fail

maybe : forall {a : Type, b : Type} 
      . (b [0..1]) -> ((a -> b) [0..1]) -> (Maybe a) -> b

The maybe function takes a default value, a function, and a Maybe value. If the Maybe value is Nothing, the function returns the default value. Otherwise, it applies the function to the value inside the Just and returns the result.

returnMb : forall {a : Type} 
         . a -> Maybe a

Monad interface for Maybe

bindMb : forall {a : Type, b : Type} 
       . (Maybe a) -> ((a -> Maybe b) [0..1]) -> Maybe b

Monad interface for Maybe

fromMaybe : forall {a : Type} 
          . (a [0..1]) -> (Maybe a) -> a

isJust : forall {a : Type} 
       . (Maybe (a [0])) -> Bool

Whether a Maybe a value is Just a

isNothing : forall {a : Type} 
          . (Maybe (a [0])) -> Bool

Whether a Maybe a value is Nothing

Meta-data

Contents