namespace http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final❚

theory Types : ur:?LF =
  tp : type❙
  tm : tp ⟶ type❘ # tm 1 prec -1❙
❚

theory Logic : ur:?LF =
  prop: type❙
  ded : prop ⟶ type❘# ⊦ 1 prec -1❘role Judgment❙
❚

theory Equality : ur:?LF =
  include ?Types❙
  include ?Logic❙
  equal : {A} tm A ⟶ tm A ⟶ prop❘# 2 = 3❙
  refl : {A,X:tm A} ⊦ X = X❙
  sym : {A,X,Y:tm A} ⊦ X = Y ⟶ ⊦ Y = X❙
  trans : {A,X,Y,Z:tm A} ⊦ X = Y ⟶ ⊦ Y = Z ⟶ ⊦ X = Z❙
  cong  : {A,B,X,Y,F:tm A ⟶ tm B} ⊦ X = Y ⟶ ⊦ (F X) = (F Y)❙
❚

theory STT : ur:?LF =
  include ?Equality❙
  
  fun : tp ⟶ tp ⟶ tp❘# 1 ⇒ 2❙
  abstract : {A,B} (tm A ⟶ tm B) ⟶ tm (A ⇒ B)❘# λ 3❙  
  apply : {A,B} tm (A ⇒ B) ⟶ tm A ⟶ tm B❘# 3 @ 4 prec 5❙
  
  beta : {A,B,F: tm A ⟶ tm B,X} ⊦ (λ F) @ X = (F X)❙
❚

theory Eta : ur:?LF =
  include ?STT❙
  eta : {A,B,F: tm (A ⇒ B)} ⊦ (λ [x: tm A] (F @ x)) = F❙
❚

theory Extensionality : ur:?LF =
  include ?STT❙
  ext : {A,B,F,G: tm (A ⇒ B)} ({x: tm A} ⊦ F @ x = G @ x) ⟶ ⊦ F = G❘# ext 5❙
❚

//  view EtaExt : ?Eta -> ?Extensionality =
  // include mmtid ?STT❙
  eta = [A,B,F] ext [x] beta❙
❚

theory List : ?STT =
  list : tp ⟶ tp❘# < 1 >❙
  nilOf : {A: tp} tm <A>❘# nil %I1❙
  cons : {A: tp} tm A ⟶ tm <A> ⟶ tm <A>❘# 2 + 3 prec 10❙
  
  fold : {A,B} tm B ⟶ (tm A ⟶ tm B ⟶ tm B) ⟶ tm <A> ⟶ tm B❙
  fold_nil : {A,B,N,C} ⊦ fold A B N C nil = N❙
  fold_cons : {A,B,N,C,X,L} ⊦ fold A B N C (X+L) = C X (fold A B N C L)❙
      
  map : {A,B} tm (A ⇒ B) ⟶ tm <A> ⟶ tm <B>❘= [A,B,f] fold A <B> nil ([a,bs] (f@a)+bs)❘# map 3 4❙
  append : {A} tm <A> ⟶ tm <A> ⇒ <A>❘= [A] fold A (<A> ⇒ <A>) (λ[x]x) ([a,f] λ[l]a+(f@l))❙
  flatten: {A} tm < <A> > ⟶ tm <A>❘= [A] fold <A> <A> nil ([l,r] (append A l) @ r)❙
❚

theory Monad : ?STT =
  operator: tp ⟶ tp❘# M 1 prec 20❙
  unit : {A} tm A ⟶ tm M A❘# return 2❙
  bind : {A,B} tm M A ⟶ tm (A ⇒ M B) ⟶ tm M B❘# 3 > 4 prec 5❙
 
  neutral_left : {A,B,F: tm (A ⇒ M B)}{X: tm A} ⊦ (return X) > F = F @ X❙
  neutral_right : {A,m: tm M A} ⊦ m > (λ [x] return x) = m❙
  assoc: {A,B,C, F: tm (A ⇒ M B), G: tm (B ⇒ M C),m: tm M A} ⊦ (m > F) > G = m > (λ[x]F @ x > G)❙ 
❚

view ListMonad : ?Monad -> ?List = 
  operator = list❙
  unit = [A] [x] x+nil❙
  bind = [A,B][l,f] (flatten B) (map f l)❙

  // neutral_left = ...❙
  // neutral_right = ...❙
  // assoc = ...❙
❚

theory MonadPlus : ?STT =
  include ?Monad❙
  // more stuff here❙
❚