data Future a = At Nat a | Never

implementation Functor Future where
    map f (At t v) = At t (f v)
    map _ Never = Never

data AndOr a b = This a | These a b | That b

race : Future a -> Future b -> Future (AndOr a b)
race (At ta a) (At tb b) = At (min ta tb) $ case compare ta tb of
    LT => This a
    EQ => These a b
    GT => That b
race (At t v) Never = At t (This v)
race Never (At t v) = At t (That v)
race Never Never = Never

mutual
    record Reactive a where
        constructor MkReactive
        initial : a
        next : Event a

    record Event a where
        constructor MkEvent
        unEvent : Future (Reactive a)

mutual
    implementation Functor Reactive where
        map f (MkReactive a next) = MkReactive (f a) $ map f next

    implementation Functor Event where
        map f (MkEvent a) = assert_total $ MkEvent $ map (map f) a

implementation Applicative Reactive where
    pure a = MkReactive a (MkEvent Never)
    rf@(MkReactive f (MkEvent nf)) <*> rv@(MkReactive v (MkEvent nv)) = assert_total $ MkReactive (f v) $ MkEvent $ flip map (race nf nv) $ \x => case x of
        This rf' => rf' <*> rv
        These rf' rv' => rf' <*> rv'
        That rv' => rf <*> rv'

implementation Monad Reactive where
    join (MkReactive (MkReactive v vs) rs) = assert_total $ MkReactive v $ MkEvent $
        flip map (race (unEvent vs) (unEvent rs)) $ \x => case x of
            This vr' => join (MkReactive vr' rs)
            These vr' _ => join (MkReactive vr' rs)
            That rs' => join rs'

rA : Reactive String
rA = MkReactive "IA" (MkEvent (At 1 (MkReactive "1A" (MkEvent Never))))

rB : Reactive String
rB = MkReactive "IB" (MkEvent (At 1 (MkReactive "1B" (MkEvent Never))))


rC1 : Reactive String
rC1 = (++) <$> rA <*> rB
--rC1 = MkReactive "IAIB" (MkEvent (At 1 (MkReactive "1A1B" (MkEvent Never)))) : Reactive String

rC2 : Reactive String
rC2 = rA >>= (\a => (a++) <$> rB)
-- MkReactive "IAIB" (MkEvent (At 1(MkReactive "IA1B" (MkEvent (At 1 (MkReactive "1AIB" (MkEvent (At 1 (MkReactive "1A1B" (MkEvent Never)))))))))) : Reactive String