forked from GitHub/gf-core
63 lines
1.8 KiB
Plaintext
63 lines
1.8 KiB
Plaintext
{-
|
|
Maybe type, modelled on Haskell
|
|
John J. Camilleri
|
|
-}
|
|
resource Maybe = open Prelude, Predef in {
|
|
|
|
oper
|
|
|
|
-- Constructors
|
|
Maybe : (t : Type) -> Type = \t -> {
|
|
inner : t ;
|
|
exists : Bool ;
|
|
} ;
|
|
Just : (T : Type) -> T -> Maybe T = \_,t -> {
|
|
inner = t ;
|
|
exists = True ;
|
|
} ;
|
|
Nothing : (T : Type) -> T -> Maybe T = \_,t -> {
|
|
inner = t ;
|
|
exists = False ;
|
|
} ;
|
|
|
|
-- IMPORTANT
|
|
-- This version of Nothing would be preferred, but it may not work as expected.
|
|
-- This happens when using Nothing within a record. For discussion of this see:
|
|
-- https://groups.google.com/d/msg/gf-dev/KAQEttN-0Cs/EjGHjOXEKO0J
|
|
Nothing' : (T : Type) -> Maybe T = \_ -> {
|
|
inner = variants {} ;
|
|
exists = False ;
|
|
} ;
|
|
-- You have been warned!
|
|
|
|
-- Functions
|
|
exists : (T : Type) -> Maybe T -> Bool = \_,m -> m.exists ;
|
|
isJust : (T : Type) -> Maybe T -> Bool = \_,m -> m.exists ;
|
|
fromJust : (T : Type) -> Maybe T -> T = \_,m -> case m.exists of {
|
|
True => m.inner ;
|
|
False => Predef.error "Called fromJust with Nothing"
|
|
} ;
|
|
fromMaybe : (T : Type) -> T -> Maybe T -> T = \_,n,m -> case m.exists of {
|
|
True => m.inner ;
|
|
False => n
|
|
} ;
|
|
|
|
-- Instance with Str, since it's common
|
|
MaybeS = Maybe Str ;
|
|
JustS : Str -> Maybe Str = \r -> Just Str r ;
|
|
-- NothingS : Maybe Str = Nothing Str ;
|
|
NothingS : Maybe Str = Nothing Str "" ;
|
|
|
|
existsS : Maybe Str -> Bool = exists Str ;
|
|
fromJustS : Maybe Str -> Str = fromJust Str ;
|
|
fromMaybeS : Str -> Maybe Str -> Str = fromMaybe Str ;
|
|
|
|
-- Example
|
|
-- j : MaybeS = JustS "hello" ;
|
|
-- n : MaybeS = NothingS ;
|
|
-- s : Str = fromJustS j;
|
|
-- b : Bool = existsS j ;
|
|
-- r : Str = if_then_Str (existsS j) ("present") ("not present") ;
|
|
|
|
}
|