qnighy

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

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

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

またサブモードとして

twixninja411

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

lukaszlew

-- 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

Lysxia

(** 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]):

echatav

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)