cont.gs
module 'cont.(type t = 'tr, ..) ∝ newtype 'm 'α. ∀ 'r. (α → m r) → m r;
-- ↓ Using Haskell-style monads is particularly useful here to show the
intimate connection between continuation-passing style and monads
instance module monad.c (cont.tr 'm) = monad.asHaskell 〈
'unit 'x = cont.in (λ 'k. k x);
'a '>>= 'f = cont.in (λ 'k. cont.out a $ λ 'x. cont.out (f x) $ k);
〉;
cont.lift.natural :: ∀ 'm1 'm2. monad.t m1 → monad.t m2 → (∀ 'α. m1 α → m2 α) → ∀ 'α. cont.tr m1 α → cont.tr m2 α;
implicit cont.lift.natural (module monad.c) (module monad.c);
'cont.lift.natural (module 'm1) (module 'm2) 'f (cont.in 'a) = cont.in (λ 'k. m2.join $ f $ a $ m1.unit ∘ k);
-- ↑ Types are:
--
-- > k :: α → m2 r
-- > m1.unit ∘ k :: α → m1 (m2 r)
-- > a $ m1.unit ∘ k :: m1 (m2 r)
-- > f $ a $ m1.unit ∘ k :: m2 (m2 r)
-- > m2.join $ f $ a $ m1.unit ∘ k :: m2 r
'fibs ∝ 0 : 1 : lift2 @list.byZip (+) fibs (drop 1 fibs);
Explanations:
- ∝ is the de-constructing bind operator.
It is also recommended for intermediate values, and is used here,
because it can have better asymptotic performance than =.
- lift2 is:
lift2 :: ∀ 'f 'α0 'α1 'β. applicative.t f → (α0 → α1 → β) → f α0 → f α1 → f β;
implicit lift2 (module applicative.c);
'lift2 'a 'f 'ax 'ay = f <$> @a ax <*> @a ay;
- @ is explicit instance application;
it allows the default, canonical structure to be over-ridden in a function.
- list.byZip is
'list.byZip = applicative.byApp 〈
'unit 'x = repeat x;
('f:'fs) '<*> ('x:'xn) :- f x : (fs <*> xn);
_ '<*> _ :- nil;
〉;
view (@@) :: ∀ 'α. α → α → α; -- > match (@@) :: ∀ 'α 'β. β → (α → α →
β) → α → β;
match (@@) 'e 'k 'x = k x x;
data 'α. | nothing | just α :: 〈
abstype t :: * → *;
nothing, view nothing, :: ∀ 'α. t α;
just, view just, :: ∀ 'α. α → t α;
〉;
Core[| data 'α. | nothing | just α |] = ⌊"Π〈
abstype t α = ⌊"Σ〈
nothing "uΠ〈〉;
just "uΠ〈 0 :: α; 〉;
〉⌋;
nothing = λ (type α :: *). ⌊"constr "Σ〈
nothing "uΠ〈〉;
just "uΠ〈 0 :: α; 〉;
〉 nothing "uΠ〈〉⌋ ⊳ "defn t α;
match nothing = λ (type α :: *). λ (type β :: *). ⌊λ (e :: β). ⌊λ (k
:: β). ⌊λ (x :: t α).
for ⌊x0⌋ ∝ x ⊳ "invert ("defn t α).
analyze x0
case nothing "uΠ〈〉. k
case _. e
⌋⌋⌋;
just = λ (type α :: *). ⌊λ (x :: α). ⌊"constr "Σ〈
nothing "uΠ〈〉;
just "uΠ〈 0 :: α; 〉;
〉 just "uΠ〈 0 = x; 〉⌋ ⊳ "defn t α⌋;
match just = λ (type α :: *). λ (type β :: *). ⌊λ (e :: β). ⌊λ (k ::
⌊α → β⌋). ⌊λ (x :: t α).
for ⌊x0⌋ ∝ x ⊳ "invert ("defn t α).
analyze x0
case just "uΠ〈 0 = x0.0; 〉. k x0.0
case _. e
⌋⌋⌋;
〉⌋;
instance module eq.c bool.t = eq.byEq 〈
bool.false '≡ bool.false :- bool.true;
bool.true '≡ bool.true :- bool.true;
_ '≡ _ :- bool.false;
〉;
instance module order.total.c bool.t = order.total.byLE 〈
bool.false '≤ 'x :- bool.true;
bool.true '≤ bool.true :- bool.true;
_ '≤ _ :- bool.false;
bool.false `'compare` bool.false :- eq;
bool.false `'compare` bool.false :- lt;
bool.true `'compare` bool.true :- eq;
bool.true `'compare` bool.false :- gt;
〉;
order.total.byLE :: ∀ 'r 'α | order.total.t α ≤ r, r ≤ 〈 (≤) :: α → α →
bool.t; 〉. r → order.total.t α;
'order.total.byLE (module 'le) = for (
'inst ∝ 〈
'x '≥ 'y = y `le.≤` x;
'x '< 'y = not (y `le.≤` x);
'x '> 'y = not (x `le.≤` x);
'x `'compare` 'y = analyze x `le.≤` y
(case true. analyze y `le.≤` x
case true. eq
case false. lt
)
case false. gt
;
〉
) module le `record.overlay` inst;
type 'iterator 'α = 〈
abstype st :: *;
start :: st;
eof :: st → bool.t;
deref :: st → α;
next :: st → st;
〉;
list.iterator :: ∀ 'α. list.t α → iterator α;
'list.iterator 'xn = 〈
abstype st = list.t α;
'start ∝ xn;
'eof nil :- true;
'eof _ :- false;
'deref !('x:'xn) = x;
'next !('x:'xn) = xn;
〉;
iterator.foldr :: ∀ 'α. (α → β → β) → β → iterator α → β;
'iterator.foldr 'f 'z (module 'it) = work it.start
where
'work 'st = analyze it.eof st
case true. z
case false. deref it `f` work (next it)
;