Incremental Behaviours

incremental-behaviours.idr

module IncrementalBehaviors

-- esempio di una prova per induzione
-- è una funzione
-- dato qualsiasi x che è un booleano
-- ritorna una equality (che sarebbe una struttra dati, leggasi new Equality(x, not(not(x))))
-- il tipo di questa funzione è la nostra ipotesi
-- se si riesce a scrivere il corpo della funzione rispettando il tipo di ritorno
-- si ottiene la prova per induzione che l'ipotesi è corretta
example : (x : Bool) -> x = not (not x)
example False = Refl
example True = Refl

namespace source
  interface EventSource (source : (event : Type) -> Type) where
    map : (mapper : eventA -> eventB) -> source eventA -> source eventB
    filter : (criteria : eventA -> Bool) -> source eventA -> source eventA

namespace behavior
  interface Behavior (behavior : (accumulator : Type) -> Type) where
    map : (mapper : accumulatorA -> accumulatorB) -> behavior accumulatorA -> behavior accumulatorB
    fold :
      EventSource source => source eventA ->
      accumulatorA -> (reducer : accumulatorA -> eventA -> accumulatorA) ->
      behavior accumulatorA

namespace incremental_behavior
  interface IncrementalBehavior (behavior : (accumulator : Type) -> (event : Type) -> (reducer : accumulator -> event -> accumulator) -> Type) where
    map :
      (mapper : accumulatorA -> accumulatorB) ->
      {delta : accumulatorA -> eventA -> eventB} ->
      {reducerA : accumulatorA -> eventA -> accumulatorA} ->
      (reducerB : accumulatorB -> eventB -> accumulatorB) ->
      {consistency :
        (a : accumulatorA) -> (e : eventA) -> (b : accumulatorB) ->
        reducerA a e = reducerB b (delta a e)
      } ->
      behavior accumulatorA eventA reducerA ->
      behavior accumulatorB eventB reducerB