Koji Miyazato viercc

Relevant definitions

data Store s a = Store (s -> a) s
fmap g (Store f s) = Store (g.f) s
extract f s = f s
duplicate (Store f s) = Store (Store f) s

Store f1 s1 <@> Store f2 s2 = Store (\s -> f1 s (f2 s2)) s1

We will also use S as a synonym for the data constructor Store

SATySFi構文メモ (2018/02/23)

SATySFiの字句解析器には主要なモードが4つある:

プログラムモード
垂直モード
水平モード
数式モード

またサブモードとして

	Given distributive categories
	* -C>, >C<, 1C, +C+, 0C
	* -D>, >D<, 1D, +D+, 0D

	An alternative functor consists of
	* A functor
	- F : C -> D
	* morphisms
	- eps : 1D -D> F(1C)
	- mu : F(a) >D< F(b) -D> F(a >C< b)

	(** Coq proof that there is no monad compatible with the ZipList applicative functor. *)
	(** Based on the original proof by Koji Miyazato https://gist.github.com/viercc/38853067c893f7ad9e0894abb543178b *)

	(** Main theorem: [No_LawfulJoin : forall join, ~(LawfulJoin join)]
	where [~] means "not" and [LawfulJoin] is the conjunction of the following properties (monad laws):

	1. [join] is associative:
	join (join xs) = join (map join xs)]

	2. [join] is compatible with ZipList's applicative (i.e., [zip_with]):

	-- Based on: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html
	import Data.List (delete, union)
	{- HLINT ignore "Eta reduce" -}

	-- File mnemonics:
	-- env = typing environment
	-- vid = variable identifier in Bind or Var
	-- br = binder variant (Lambda or Pi)
	-- xyzTyp = type of xyz
	-- body = body of Lambda or Pi abstraction