-
Notifications
You must be signed in to change notification settings - Fork 5
/
Maybe.fm
76 lines (61 loc) · 2.09 KB
/
Maybe.fm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
// The Maybe(A) type can hold a value of type A or nothing.
T Maybe <A: Type>
| Maybe.none;
| Maybe.some(value: A);
Maybe.bind<A: Type, B: Type>(m: Maybe(A), f: A -> Maybe(B)): Maybe(B)
case m:
| Maybe.none<B>;
| f(m.value);
Maybe.pure<A: Type>(a: A): Maybe(A)
Maybe.some<A>(a)
// the monad instance for Maybe
Maybe.monad: Monad(Maybe)
Monad.new<Maybe>(Maybe.bind, Maybe.pure)
Maybe.extract<A: Type>(m: Maybe(A), a: A): A
case m:
| a;
| m.value;
Maybe.join<A: Type>(m: Maybe(Maybe(A))): Maybe(A)
case m:
| Maybe.none<A>;
| m.value;
Maybe.map<A: Type, B: Type>(f: A -> B, m: Maybe(A)): Maybe(B)
case m:
| Maybe.none<B>;
| Maybe.some<B>(f(m.value));
Maybe.IsSome(A: Type,x: Maybe(A)): Type
case x:
| Empty;
| A;
Maybe.some_isnt_none<A: Type>(x: A) : Not(Equal(Maybe(A),Maybe.some<A>(x),Maybe.none<A>))
def P = ((x) case x: | Empty; | Unit;) :: Maybe(A) -> Type
(e) Equal.rewrite<Maybe(A), Maybe.some<A>(x), Maybe.none<A>,P>(e, Unit.new)
Maybe.is_some<A: Type>(x: A): Maybe.IsSome(A,Maybe.some<A>(x))
def y = Maybe.some<A>(x)
case y:
with e : Equal(Maybe(A),y,y.self) = Equal.to<Maybe(A),y>;
| Empty.absurd<>(Maybe.some_isnt_none<A>(x,e));
| y.value;
// Maybe functor
// =============
// The functor instance for maybe
Maybe.functor: Functor(Maybe)
Functor.new<Maybe>(Maybe.map)
// Proof that Maybe.functor conforms to the functor laws
Maybe.functor.verified: VerifiedFunctor(Maybe, Maybe.functor)
VerifiedFunctor.new<Maybe, Maybe.functor>(Maybe.map.id, Maybe.map.comp)
Maybe.map.id<A: Type>(ma: Maybe(A)): Equal(Maybe(A), Maybe.map<A, A>(Function.id<A>, ma), ma)
case ma:
| _;
| _;
: Equal(_, Maybe.map<,>(Function.id<>, ma.self), ma.self);
Maybe.map.comp<A: Type, B: Type, C: Type>(ma: Maybe(A), g: (B -> C), h: (A -> B))
: Equal(Maybe(C),
Maybe.map<A, C>(Function.comp<A, B, C>(g, h), ma),
Function.comp<Maybe(A), Maybe(B), Maybe(C)>(Maybe.map<B, C>(g), Maybe.map<A, B>(h))(ma))
case ma:
| _;
| _;
: Equal(_,
Maybe.map<,>(Function.comp<,,>(g, h), ma.self),
Function.comp<,,>(Maybe.map<,>(g), Maybe.map<,>(h))(ma.self));