.gitignore

*.agdai
agda-stdlib-*

add.agda

module Add where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)


data Nat : Set where
  Z : Nat
  S : Nat -> Nat

plus : Nat -> Nat -> Nat
plus Z n = n
plus (S n) m = S (plus n m)

lem-plus-z : ∀ (a : Nat) -> plus a Z ≡ a
lem-plus-z Z = refl
lem-plus-z (S a) rewrite lem-plus-z a = refl

lem-plus-suc : ∀ (a b : Nat) -> plus a (S b) ≡ S (plus a b)
lem-plus-suc Z b = refl
lem-plus-suc (S a) b rewrite lem-plus-suc a b = refl

-- Commutativity
plus-commutes : ∀ (a b : Nat) -> plus a b ≡ plus b a
plus-commutes a Z = lem-plus-z a
plus-commutes a (S b) rewrite lem-plus-suc a b | plus-commutes a b = refl

-- Associativity
plus-associates : ∀ (a b c : Nat) -> plus a (plus b c) ≡ plus (plus a b) c
plus-associates Z b c = refl
plus-associates (S a) b c rewrite plus-associates a b c = refl

mult : ∀ (a b : Nat) -> Nat
mult Z _ = Z
mult (S m) n = plus n (mult m n)


lem-mult-zero : ∀ (a : Nat) -> mult a Z ≡ Z
lem-mult-zero Z = refl
lem-mult-zero (S a) rewrite lem-mult-zero a = refl

lem-mult-suc : ∀ (a b : Nat) -> mult a (S b) ≡ plus a (mult a b)
lem-mult-suc Z b = refl
lem-mult-suc (S a) b rewrite lem-mult-suc a b
                           | plus-associates a b (mult a b)
                           | plus-associates b a (mult a b)
                           | plus-commutes a b
                           = refl

-- Commutativity
mult-commutes : ∀ (a b : Nat) -> mult a b ≡ mult b a
mult-commutes a Z rewrite lem-mult-zero a = refl
mult-commutes a (S b) rewrite lem-mult-suc a b | mult-commutes a b = refl

-- Distributivity
mult-distributes-right : ∀ (a b c : Nat) -> mult a (plus b c) ≡ plus (mult a b) (mult a c)
mult-distributes-right a Z c rewrite lem-mult-zero a = refl
mult-distributes-right a (S b) c rewrite mult-commutes a (plus (S b) c)
                                       | mult-commutes (plus b c) a
                                       | mult-distributes-right a b c
                                       | lem-mult-suc a b
                                       | plus-associates a (mult a b) (mult a c) = refl

mult-distributes-left : ∀ (a b c : Nat) -> mult (plus a b) c ≡ plus (mult a c) (mult b c)
mult-distributes-left a b c rewrite mult-commutes (plus a b) c
                                  | mult-commutes a c
                                  | mult-commutes b c 
                                  | mult-distributes-right c a b = refl

-- Associativity
mult-associates : ∀ (a b c : Nat) -> mult a (mult b c) ≡ mult (mult a b) c
mult-associates Z b c = refl
mult-associates (S a) b c rewrite mult-associates a b c
                                | mult-distributes-left b (mult a b) c = refl

ArrowTypechecker.hs

{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
{-# Language Arrows, GADTs, DataKinds, KindSignatures, TypeOperators #-}

import Control.Arrow
import Lens.Micro
import qualified Data.Either
import Prelude hiding (Left, Right)

class Type a where
  --kind :: a p -> a p
  --isStar :: a -> Bool
  exponential :: a -> a -> a
  var :: a
  exp :: Lens' a a
  base :: Lens' a a


class Arrow tc => TypeChecker tc where
  -- what are the TC methods supposed to be? Lenses? Prisms?
  -- We need to be able to focus into the exponent, but the result should be an error type
  -- attach builds the space (groupoid)
  --attach :: ({-Place a, Place b, -}Type t) => t `tc` t -> t `tc` t -> ()
  attach :: ({-Place a, Place b, -}Type t) => t -> t -> (t `tc` u) -> u -- similar to `seq` or `traceShowId`

{-
class {-TypeChecker lc =>-} LC lc where
  app :: lc a b -> lc c d -> lc f g
  lam :: (lc a b -> lc c d) -> lc f g

data E a b where
  Var :: String -> E a b
  Lam :: (E a b -> E c d) -> E f g
  App :: E a b -> (E c d -> E f g)
  IntLit :: E a b
-}

data Dir = Left Dir | Right Dir | IntDir

class Place (p :: Dir)

instance Place p => Place (Left p)
instance Place p => Place (Right p)
instance Place IntDir


class {-TypeChecker lc =>-} LC lc where
  app :: Place p => lc (Left p) -> lc (Right p) -> lc p
  lam :: Place p => (lc (Left p) -> lc (Right p)) -> lc p
  tc :: (Type t, TypeChecker tc) => Place p => lc p -> tc t t



data E d where
  Var :: String -> E d
  Lam :: (E (Left d) -> E (Right d)) -> E d
  App :: E (Left d) -> (E (Right d) -> E d)
  IntLit :: E IntDir -- this won't work at the end of the day.. placeholder for now


instance LC E where
  app = App; lam = Lam
  tc IntLit = arr id
  tc (App f a) = proc t -> do let tf = t `exponential` var
                              tf' <- tc f -< tf
                              returnA -< tf' ^. base


data Ty = IntTy | ArrTy Ty Ty | VarTy | ErrTy [String] deriving Show

instance Type Ty where
  var = VarTy
  exponential = ArrTy
  exp = expo


instance TypeChecker (->)

tcTestInt :: Ty -> Ty
tcTestInt = tc IntLit


-- * EXPERIMENT with lenses
-- gather some intuition how lenses work with type checking
-- ** case study: get the exponent (i.e. domain of the arrow)
-- one of the interesting questions is where unification should happen
-- - in the getter or
-- - the setter
-- part of the lens?
-- since in the setter the type is being rebuilt, one could
-- - accumulate errors
-- - augment constraints
-- there.

-- *** easiest case: ArrTy

expo :: Lens' Ty Ty
expo = expoGet `lens` expoSet

-- expoArr = lens (\(a `ArrTy` b) -> a) (\(_ `ArrTy` b) a -> a `ArrTy` b)

-- *** exponent of an ErrTy is an ErrTy
-- and by setting it, it won't improve!
-- However one could track where the error comes from,
-- and the fact that it should have an exponent is a useful bit.

-- expoErr = lens (\ErrTy -> ErrTy) (\ErrTy _ -> ErrTy)

-- *** exponent of an IntTy is an ErrTy
-- and it should probably taint the Int when set.

-- expoInt = lens (\IntTy -> ErrTy) (\IntTy _ -> ErrTy) -- not so sure

-- *** exponent of a VarTy is a VarTy
-- and it should track the constraint that the original variable is now an arrow.

-- expoVar = lens (\VarTy -> VarTy) (\VarTy a -> a `ArrTy` VarTy)

expoGet (a `ArrTy` b) = a
expoGet (ErrTy es) = ErrTy ("not a function type":es)
expoGet IntTy = ErrTy ["Int is not n arrow type"]
expoGet VarTy = VarTy -- FIXME: fresh

--expoSet :: forall tc. TypeChecker tc => Ty -> Ty -> Ty
--expoSet (a' `ArrTy` b) a = attach a a' (arr @tc (`ArrTy` b)) -- FIXME: unify a' and a
expoSet (a' `ArrTy` b) a = a `ArrTy` b -- FIXME: unify a' and a
expoSet (ErrTy _) _ = ErrTy []
expoSet IntTy _ = ErrTy []
expoSet VarTy a = a `ArrTy` VarTy

-- ** Unificator: a lens
-- getter is the identity
-- setter unifies
-- can we reformulate expo by having [a `attach` (va' -> va'')] and va' `unify` exponent?

unifTy :: Lens' Ty Ty
unifTy = lens id unify
  where unify IntTy IntTy = IntTy

-- ** What about the lens laws?
-- we can only call these lenses when they satisfy the laws
-- otherwise it is just abuse of notation

-- * TESTs

t1 = set expo IntTy (VarTy `ArrTy` IntTy)
t2 = set expo IntTy (IntTy `ArrTy` IntTy)

main = do print t1
          print t2

Chinese.hs

import Data.List (find)
import Debug.Trace

data Ideal a = Ide (a, a) deriving Show

instance (Show a, Integral a) => Semigroup (Ideal a) where
  Ide (a, ar) <> Ide (b, br) = Ide (c, cr `mod` c)
    where common = (,) <$> norm (take (fromIntegral (c `div` a)) [ar, ar + a ..]) <*> norm (take (fromIntegral (c `div` b)) [br, br + b ..])
          c = a `lcm` b
          Just (cr, _) = find (uncurry (==)) common
          norm = ((`mod` c) <$>)

t1 = Ide (2, 1) <> Ide (3, 2)
t2 = Ide (2, -1) <> Ide (3, 2)


test = Ide (3, 2) <> Ide (7, 6) <> Ide (17, 6) <> Ide (23, 10)
test2 = Ide (3, 2) <> Ide (7, 0) <> Ide (17, 6) <> Ide (23, 7)

Globular.agda

module Globular where

--open import Agda.Builtin.Equality renaming (_≡_ to _==_)
--open import Data.Product

mutual

 data Ty : Set where
   ★ : Ty
   Ar : Ty → Name → Name → Ty

 -- names are just the list of types leading to an entry in a context
 infixl 4 _▷_
 data Name : Set where
   ∙ : Name
   _▷_ : Name → Ty → Name

-- * Contexts

-- Syntactically contexts are just a Name

-- * Pasting schemes
-- We have (complete) pasting schemes and partial pasting schemes.
-- the latter have an (n-dimensional) object in /focus/.

-- For our purposes a pasting scheme is a =Context= built by the below methods.

-- Well-formed (partial) pasting schemes can be built by means of copatterns
-- from partial pasting schemes

-- down: decrease dimension, focus on the target of the focus.
-- up: build an (n+1 dimensional) morphism by creating a new object with same type
--     as the focus, connecting them with the morphism and leaving it in focus.

-- wrap: make a pasting scheme from a partial one by discarding a trivial (i.e. ★-typed)
--       focus

-- into: start a partial pasting scheme with a point in focus.

-- a partial pasting scheme
data PPS : Name → Name → Ty → Set where
  ∙,★ : PPS (∙ ▷ ★) ∙ ★
  up : ∀ {ns foc t} → PPS ns foc t → PPS (ns ▷ t ▷ Ar t foc ns) (ns ▷ t) (Ar t foc ns)
  down : ∀ {ns foc t sou tar} → PPS ns foc (Ar t sou tar) → PPS ns tar t

data PS : Name → Set where
  wrap : ∀ {ns foc} → PPS ns foc ★ → PS ns

sc1 = wrap (down (down (up (up ∙,★))))
sc2 = wrap (down (up (down (down (up (up ∙,★))))))

Globular.hs

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ConstraintKinds, TypeApplications #-}
{-# LANGUAGE PartialTypeSignatures, UndecidableInstances, FlexibleInstances, MultiParamTypeClasses, TypeFamilies #-}
{-# language KindSignatures, DataKinds, PolyKinds, GADTs, TypeOperators, RankNTypes, ViewPatterns #-}

-- See http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/docs/mimram_catt.pdf

module Globular where

import GHC.TypeLits
import GHC.Exts
import Data.List (tails, lookup)
import Data.Maybe (fromJust)
import Debug.Trace


-- * Peano with End

-- See: http://bentnib.org/binding-universe.html
-- can we do something similar in Haskell?

--type End f = forall a . f a
type End f a = f a
type End2 f a = f a -> f a


data {-kind-} ℕ = ℤ | 𝕊 ℕ

data PeanoK :: k -> * where
  Zero :: End PeanoK a
  -- Succ :: End2 PeanoK a -- DOESN'T WORK :-(

 -- END EXPERIMENT



data Tag = Tm Nat | Ty Nat | Cxt [Nat] | Sbst [Nat]

data Globe :: Tag -> * where
  Star :: Type 0
  Hom :: Type n -> Term n -> Term n -> Type (n+1)
  Var :: String -> Type n -> Term n
  Empty :: Context '[]
  Expand :: Context ns -> (Term n, Type n) -> Context (n : ns)

type Context l = Globe (Cxt l)
type Term n = Globe (Tm n)
type Type n = Globe (Ty n)
type Substitution l = Globe (Sbst l)

infixl 5 `Expand`

-- * Building globular sets by monadic operations

data Builder :: * -> * where
  (:-) :: Context l -> focus -> Builder focus -- {|-}_ps

infix 3 :-

instance Functor Builder where
  fmap f (e :- foc) = e :- f foc

instance Applicative Builder where
  pure = (Empty :-)

instance Monad Builder where
  e :- foc >>= f = case f foc of
                     Empty :- foc' -> e :- foc'
                     Empty `Expand` l `Expand` h :- foc' -> e `Expand` l `Expand` h :- foc'

type TypedTerm n = (Term n, Type n)
up :: String -> String -> Builder (TypedTerm n)
up = undefined

-- * Recreating the deduction system from page 3
--
--

data Typ = S | Typ ::> Typ
infix 2 ::>


-- Well-formed context: Γ ⊢

class WellFormed (ctx :: [(Symbol, Typ)])
instance WellFormed '[]
instance (ctx ⊢ t) => WellFormed ('(x, t) : ctx)

-- Well-formed type in context: Γ ⊢ A

class (ctx :: [(Symbol, Typ)]) ⊢ (ty :: Typ)
infix 1 ⊢
instance WellFormed ctx => ctx ⊢ S
instance (ctx ⊢ t, ctx ⊢ u) => ctx ⊢ (t ::> u)

-- Typed terms (vars only for now) in context: Γ ⊢ t : A

type family ctx ⊢: vty where
  (vty : ctx) ⊢: vty = WellFormed (vty : ctx)
  (utx : ctx) ⊢: vty = ctx ⊢: vty
infix 1 ⊢:


-- ** Tests
--
data Evidence :: Constraint -> * where
  Evidence :: c => Evidence c
  SameVTY :: (((vty : ctx) ⊢: vty) ~ WellFormed (vty : ctx)) => Evidence ((vty : ctx) ⊢: vty)

deriving instance Show (Evidence c)

te0 = Evidence @ ('[] ⊢ S ::> S)
te1 = Evidence @ ('[ '("x", S) ] ⊢ S ::> S)
te2 = Evidence @ ('[ '("x", S) ] ⊢: '("x", S))
te3 = Evidence @ ('[ '("h", S), '("x", S) ] ⊢: '("x", S))
te4 = Evidence @ ('[ '("h", S), '("x", S) ] ⊢: '("h", S))
-- If Γ ⊢ t : A holds then Γ ⊢ A holds.
--lemma61 :: Evidence (ctx ⊢: '(t, a)) -> Evidence (ctx ⊢ a)
--lemma61 SameVTY = Evidence

-- * Building globular sets by PHOAS

-- the idea is that whenever we increase the dimension we get two new
-- bindings in scope, for every x of type A a new (y : A) and a morphism
-- (f : x -->_A y)
-- E.g. newStar (\x -> raise x $ \y f -> ...)
-- of course these must be monadic operations, since the context must be managed:
-- do { x <- newStar; (y, f) <- raise; target y }
-- Ideally a De Bruijn level (?) would become visible in each variable's type
-- Also the monadic actions probably won't work, since we have two type parameters.
-- Overloaded syntax for "do" might help.

-- But let's start with a simpler task first


-- The =GTy= kind describes the possible types of globular cells.
-- We refer to named cells by mentioning the prefix of the context leading
-- up to it. This is a De Bruijn-like notation (De Bruijn levels). In Haskell
-- we use the kind =[GTy]=. The latter being cons-lists we actually having
-- suffixes :-(, where contexts should be snoc-lists actually.

--                +-- name of source face
--                |
--                |        +-- name of target face
--                |        |
--                |        |
--                v        v
data GTy = St | [GTy] :> [GTy]
 deriving (Eq, Show)

infix 4 :>

-- Note: Since we are using De Bruijn levels, the coherence condition is simpler:
--       coh_G_{x -> y_A} when the type is derivable and x <= y (index comparison).

-- TODO: We can eliminate the third argument of =(:>)= because we observe that
--       the head of both variable mentions must necessarily contain that type.

--                        +-- types in context (pasting scheme)
--                        |
--                        |        +-- type of focus
--                        v        v
class HasContext (ctx :: [GTy] -> GTy -> *) where
  newStar :: (ctx '[St] St -> ctx many St) -> ctx many St
  raise :: ctx (a:c) a
        -> (ctx (a:a:c) a -- TODO: y and f should live in the same context
         -> ctx ((a:c :> a:a:c):a:a:c) (a:c :> a:a:c)
         -> ctx many a)
        -> ctx many a
  lengthen :: ctx ((x:xs :> x:ys):c) a -- TODO: a should be x
        -> (ctx ((x:ys :> a:(x:xs :> x:ys):c):a:(x:xs :> x:ys):c) a
         -> ctx ((x:ys :> a:(x:xs :> x:ys):c):a:(x:xs :> x:ys):c) (x:ys :> a:(x:xs :> x:ys):c)
         -> ctx many a)
        -> ctx many a
  refocus :: {- less `SomewhereIn` (a :c) => -} ctx many (n :> m) -> ctx (b:other) b -> ctx many b
  target :: ctx ((c :> a:c):a:c) (c :> a:c) -> ctx (a:c) a -> ctx ((c :> a:c):a:c) a
  target = refocus

-- Using this vocabulary will result in alpha-conversion invariant globular pasting schemes. This is
-- guaranteed by parametricity.


-- Possibly improved idea:
--  start with a source point x --> HOAS call with f : x -> y
--  must return y by calling 'target f'
--      or 'inflate' with HOAS callback being passed an alpha : f -> f'
--                        which needs to return f' by using target
-- the environment is populated in Dyck words order (we can do this because of De Bruijn levels) -- NOO: causes infinite types!

--                       +-- types in context (pasting scheme)
--                       |
--                       |        +-- object in focus (as a De Bruijn level)
--                       v        v
class Globular (ctx :: [GTy] -> [GTy] -> *) where
  startPoint :: ctx '[St] '[St]
  fromPoint :: (ctx '[ '[St]:>'[St, St], St, St] '[ '[St]:>'[St, St], St, St] -> ctx many [St, St]) -> ctx many [St, St]
  fromPoint = inflate startPoint
  itsTarget :: ctx env ((s:>t):others) -> ctx env t
  inflate :: (t ~ (st:env), arr ~ ((st:others:>t):t)) => ctx env (st:others) -> (ctx arr arr -> ctx more t) -> ctx more t

-- Tests

-- .->.
modern1 :: Globular ctx => ctx '[ '[St] :> '[St, St], St, St] '[St, St]
modern1 = fromPoint itsTarget

-- inflate surely looks like monadic 'bind'
-- .(->||->).
modern2 :: Globular ctx => ctx '[ '[ '[St] :> '[St, St], St, St] :> '[ '[St] :> '[St, St], '[St] :> '[St, St], St, St], '[St] :> '[St, St], '[St] :> '[St, St], St, St]
                        '[St, St]
modern2 = fromPoint (\f -> itsTarget (inflate f itsTarget))

-- .(->||->||->).
modern2a :: Globular ctx => ctx _ _
modern2a = fromPoint (\f -> itsTarget (inflate (inflate f itsTarget) itsTarget))



glob1 :: HasContext ctx => ctx '[ '[St] :> '[St, St], St, St] St
glob1 = newStar (\x -> raise x (\y f -> f `target` y))

glob2 :: HasContext ctx => ctx '[ '[ '[St] :> '[St,St],St,St] :> '[ '[St] :> '[St,St],'[St] :> '[St,St],St,St],'[St] :> '[St,St],'[St] :> '[St,St],St,St] St
glob2 = newStar (\x -> raise x (\y f -> raise f (\g alpha -> alpha `target` g) `refocus` y))

glob3 :: HasContext ctx => ctx '[ '[ '[ '[St] :> '[St,St],St,St] :> '[ '[St] :> '[St,St],'[St] :> '[St,St],St,St],'[St] :> '[St,St],'[St] :> '[St,St],St,St] :> '[ '[ '[St] :> '[St,St],St,St] :> '[ '[St] :> '[St,St],'[St] :> '[St,St],St,St],'[ '[St] :> '[St,St],St,St] :> '[ '[St] :> '[St,St],'[St] :> '[St,St],St,St],'[St] :> '[St,St],'[St] :> '[St,St],St,St],'[ '[St] :> '[St,St],St,St] :> '[ '[St] :> '[St,St],'[St] :> '[St,St],St,St],'[ '[St] :> '[St,St],St,St] :> '[ '[St] :> '[St,St],'[St] :> '[St,St],St,St],'[St] :> '[St,St],'[St] :> '[St,St],St,St] St
glob3 = newStar (\x -> raise x (\y f -> raise f (\g alpha -> raise alpha (\beta pHI -> pHI `target` beta) `refocus` g) `refocus` y))

-- whisker at end
glob1' :: HasContext ctx => ctx '[ '[St,St] :> '[St,'[St] :> '[St,St],St,St],St,'[St] :> '[St,St],St,St] St
glob1' = lengthen glob1 (\z h -> z)

glob1'' :: HasContext ctx => ctx '[ '[St,'[St] :> '[St,St],St,St] :> '[St,'[St,St] :> '[St,'[St] :> '[St,St],St,St],St,'[St] :> '[St,St],St,St],St,'[St,St] :> '[St,'[St] :> '[St,St],St,St],St,'[St] :> '[St,St],St,St] St
glob1'' = lengthen glob1' (\w i -> w)

-- build .-->.-->. inside newStar (without returning first)

glob11 :: HasContext ctx => ctx '[ '[St,St] :> '[St,'[St] :> '[St,St],St,St],St,'[St] :> '[St,St],St,St] St
glob11 = newStar (\x -> raise x (\y f -> lengthen (f `target` y) (\z g -> z)))


-- build |==>|==>|

glob212 :: HasContext ctx => ctx '[ '[ '[St] :> '[St,St],'[St] :> '[St,St],St,St] :> '[ '[St] :> '[St,St],'[ '[St] :> '[St,St],St,St] :> '[ '[St] :> '[St,St],'[St] :> '[St,St],St,St],'[St] :> '[St,St],'[St] :> '[St,St],St,St],'[St] :> '[St,St],'[ '[St] :> '[St,St],St,St] :> '[ '[St] :> '[St,St],'[St] :> '[St,St],St,St],'[St] :> '[St,St],'[St] :> '[St,St],St,St] St
glob212 = newStar (\x -> raise x (\y f -> raise f (\g alpha -> lengthen (alpha `target` g) (\h beta -> h)) `refocus` y))



-- * Computing the Dimension

type family Dim (ty :: GTy) :: Nat where
  Dim St = 0
  Dim ((ty : s) :> (ty : t)) = Dim ty + 1


-- * Computing the Source of a Pasting Scheme

-- http://blogs.ams.org/visualinsight/2015/07/15/dyck-words

{- Dyck words!
    . . .
   . o . o                      . - . -
  o ó ò ó ò    2-dim source:   o ó - ó -   -- simplify:  o o o
 o o . o . o                  o o . o . o               o o o o
o . . . . . o                o . . . . . o             o . . . o

    . . .
   . o . o                      . - . -
  o o o o o                    - - - - -
 ó o . o . ò   1-dim source:  ó - . - . -
o . . . . . o                o . . . . . o

    .
   o .                       -
  ó ò o     1-dim source    ó - o   -- simplify:  o o
 o . o o                   o . o o               o o o

N.B. in a De Bruijn context simplification does not make sense.
     Instead a blacklisting can be performed.

-}
type family Source (ctx :: [GTy]) :: [GTy] where


-- * Computing the Target of a Pasting Scheme

{-

    . . .
   . o . o                      . - . -
  o ó ò ó ò    2-dim source:   o - ò - ò
 o o . o . o                  o o . o . o
o . . . . . o                o . . . . . o

    . . .
   . o . o                      . - . -
  o o o o o                    - - - - -
 ó o . o . ò   1-dim target:  - - . - . ò
o . . . . . o                o . . . . . o

.
   o .                       -
  ó ò o     1-dim target    - ò o   -- simplify:  o o
 o . o o                   o . o o               o o o

-}

-- * Computing the De Bruijn Index

class DeBruijn (env :: [k]) (var :: [k]) where
  type Index env var :: Nat

--instance (env ~ var) => DeBruijn env var where type Index env var = 0

instance DeBruijn env var => DeBruijn (t : env) var where type Index (t : env) var = Index env var + 1


-- * Show it

data PrintCtx :: [GTy] -> GTy -> * where
  Env :: [GTy] -> PrintCtx many f

instance HasContext PrintCtx where
  newStar f = f (Env [St])
  raise (Env e@(ty : _)) f = f (Env ye) (Env $ g : ye)
    where g = e :> ye -- TODO: check other side too
          ye = ty : e
  lengthen (Env e@((:>) _ ye@(ty:_) : _)) f = f (Env ze) (Env $ h : ze) -- TODO: check other side too
    where h = ye :> ze
          ze = ty : e
  refocus (Env ctx) _ = Env ctx

showCtx :: {-HasContext ctx => ctx-}PrintCtx c f -> String
showCtx (Env ctx) = show ctx


pretty :: [GTy] -> [(Char, String)]
pretty rvs = result
  where vs = reverse rvs
        result = zipWith pairWithName [0..] vs
        names = fst <$> result
        pairWithName n v = (letters !! d !! n, prettyType v)
          where d = dim v
        dim St = 0
        dim (t:_ :> _) = 1 + dim t
        letters = [ ['x' .. 'z'] ++ ['v' .. 'w'] ++ ['a'..]
                  , ['f'..]
                  , ['α'..]
                  , ['Θ'..] ]
        ts = zip (tail . reverse $ tails rvs) names
        
        prettyType St = "*"
        prettyType (s :> t) = "(" ++ pure (fromJust (lookup s ts)) ++ " --> " ++ pure (fromJust (lookup t ts)) ++ ")"
        

prettyCtx :: {-HasContext ctx => ctx-}PrintCtx c f -> [(Char, String)]
prettyCtx (Env ctx) = pretty ctx

-- * Can we HOAS-build opetopic pasting schemes?
--        g
--     b --- c
--   / f       \ h
-- a ----------> d

{-
  do ad :: ((a -> b -> c -> d) -> something) <- points -- start with 0-dimensional data
     cards (ad $ \ f g h -> card (g, h)) -- add a card below g and h
     

  zero (\a -> add (\b -> add (\c -> add (\d -> done))))
-}

-- * A small diversion: STLC

-- Again, contexts are cons-lists (i.e. reversed). Variable mentions are De Bruijn
-- levels (i.e. earlier vars have shorter names).

-- This time let's do some inference too. (If possible.)
-- Everything is PHOAS as above.

-- Note: For inference I'll leave away the latter parameter,
--       but in the meantime let's polish this out a bit
--       and see where we'll get.

class STLC (lc :: [*] -> * -> *) where
  lam :: (lc (a:ctx) a -> lc (a:ctx) b) -> lc ctx (a -> b)
  app :: lc ctx'' (a -> b) -> lc ctx' a -> lc ctx b

  plus :: lc '[] (Integer -> Integer -> Integer)
  lit :: a -> lc '[] a

infixl 8 `app`

lc0 :: STLC lc => lc '[] Integer
lc0 = plus `app` lit 1 `app` lit 41

lc1 :: STLC lc => lc '[] (Integer -> Integer)
lc1 = lam (plus `app` lit 1 `app`)


-- ** Implement

newtype Val (ctx :: [*]) a = Val a

instance STLC Val where
  lam f = Val $ \(f . Val -> Val b) -> b
  Val f `app` Val a = Val $ f a
  lit = Val
  plus = Val (+)


compile :: (forall lc . STLC lc => lc '[] a) -> a
compile lc = it
  where Val it = lc

-- it works: compile (lc1 `app` lit 4)


-- ** Inference

data STLCTy = Integer | STLCTy :-> STLCTy | TyVar deriving Show

class InEnv v where
  ty :: v -> STLCTy -> STLCTy

instance InEnv (Val '[] Integer) where
  ty _ Integer = Integer
  ty _ TyVar = Integer -- bind it!
  ty _ unexp = traceShow unexp Integer



instance InEnv (Val (n:ctx) n) where
  ty _ Integer = Integer
  ty _ wha = traceShow (show wha) TyVar

Graph.hs

{-# language FlexibleInstances, FlexibleContexts, RecursiveDo, UndecidableInstances, TypeFamilies, TypeOperators #-}

import Control.Monad.Fix
import Control.Arrow
import Data.Map (alter, union, unionWith, empty, Map, insert, foldrWithKey, mapWithKey, elems, lookup, fromList)
import Data.Set (Set, toList)
import qualified Data.Set as Set
import Data.List (group, notElem)
import Data.Maybe (catMaybes)
import Control.Monad.State
import Debug.Trace (traceShow, traceShowId)

primes :: Integral n => [n]
primes=2:[ p|p<-[3,5..],all((/=0).(rem$p))$takeWhile((<=p).(^2))primes]

primeFactors :: Integral n => [n] -> n -> [n]
primeFactors acc 1 = acc
primeFactors acc n = primeFactors (f : acc) q
  where ((q,_), f):_ = filter ((==0).snd.fst) $ map ((n `quotRem`) &&& id) primes

class MonadFix m => Graph m where
  data Object m
  object :: m (Object m)
  morph :: Object m -> Object m -> m ()
  graph :: m [Object m]

grph, grph2, grph4 :: Graph m => m [Object m]
grph = do n1 <- object
          n2 <- object
          m <- n1 `morph` n2
          graph
grph2 = mdo m <- n1 `morph` n2
            n1 <- object
            n2 <- object
            graph
grph4 = do a <- object
           b <- object
           c <- object
           d <- object
           a `morph` b
           a `morph` c
           b `morph` c
           b `morph` d
           c `morph` d
           graph

-- implement Graph for the "prime transport category"
-- grph will be [2, 6]

type GS = State ([Integer], Integer `Map` Set Integer)
instance Graph GS where
  newtype Object GS = O Integer deriving Show
  object = do p <- state $ head . fst &&& first tail
              pure $ O p
  graph = do p:_ <- fst <$> get
             let candidates = takeWhile (<p) primes
             pure . map O $ candidates
             get >>= pure . map (O . product) . elems . fixpoint' candidates . snd


  O dom `morph` O cod = modify' $ second (register dom cod)

register :: (Ord k, Ord v) => k -> v -> Map k (Set v) -> Map k (Set v)
register k v = Data.Map.alter go k
  where go Nothing = pure $ Set.singleton v
        go s = Set.insert v <$> s

fixpoint' :: [Integer] -> Integer `Map` Set Integer -> Map Integer [Integer]
fixpoint' ps0 mors = step ps ps mors
  where ps = fromList . map (id &&& pure) $ ps0
        step a c ms = let r = fixpoint a c ms in
                        if null r then a else
                          traceShow (mors, "iter", r, r `union` a, fixpoint (r `union` a) r ms)
                          $ step (r `union` a) r ms
fixpoint :: Map Integer [Integer] -- all ps
         -> Map Integer [Integer] -- todo list
         -> Integer `Map` Set Integer -- morphisms
         -> Map Integer [Integer]
fixpoint acc cur mors = foldrWithKey go empty cur
  where go :: Integer -> [Integer] -> Map Integer [Integer] -> Map Integer [Integer]
        go p fs = case check of
                    Nothing -> id
                    Just f -> f
          where check :: Maybe (Map Integer [Integer] -> Map Integer [Integer])
                check = do cods <- toList <$> Data.Map.lookup p mors
                           let go cod = do cops <- Data.Map.lookup cod acc
                                           -- blow a bunch of factors into the codomain's factor and see if the stick
                                           let transport = if missing then Just (concat $ elems $ smash) else Nothing
                                                 where mcop = fromList $ (head &&& id) <$> group cops
                                                       mfs = mapWithKey (:) $ fromList $ (head &&& id) <$> group fs
                                                       smash = unionWith shorter mcop mfs
                                                       shorter as bs = if length as < length bs then as else bs
                                                       missing = traceShow (mcop, smash) $ mcop /= smash

                                           insert cod <$> transport
                           pure $ foldl (.) id (catMaybes $ go <$> cods)


g, g2, g3, g4 :: [Object GS]
g = fst $ runState grph (primes, empty)
g2 = fst $ runState grph2 (primes, empty)
g3 = fst $ flip runState (primes, empty) $
            do o <- object
               p <- object
               dia <- object
               o `morph` p
               p `morph` dia
               dia `morph` p
               graph
g4 = fst $ runState grph4 (primes, empty)

main = print $ g4

-- TODO:
-- - use multimap (Map Int (Set Int))

hyperfunc.hs

{-# language ScopedTypeVariables #-}


import Data.Char
import Control.Category
import Control.Monad.Fix


type Hy0 a = a -> a

ex1, ex2 :: Hy0 Int
ex1 _ = 42     -- ignore argument
ex2 i = i + 42 -- use argument


-- Let's make 'use argument' a bit fancier
{-
type Hy a b = Hy b a -> b
ex3, ex4 :: Hy Char Int
ex3 _ = 42                   -- ignore hyperfunction
ex4 hy = ord (invoke hy 25)  -- use hyperfunction

-- >>> Cycle in type synonym declarations:
-}


{- ## Basic intuition

(forall a . a -> b) _is essentially_ b
and (forall b . b -> a) _is essentially_ a
so a -> b is essentially (forall b . b -> a) -> b

We are now specializing the inner b to (forall a . a -> b)
 getting ((forall a . a -> b) -> a) -> b
and then the same with innermost a, alternating ad infinitum


-}


newtype Hy a b = Hy (Hy b a -> b)

ex3, ex4 :: Hy Char Int -> Int
ex3 _ = 42              -- ignore hyperfunction
ex4 hy = invoke hy 'K'  -- use hyperfunction



invoke :: Hy a b -> (a -> b)
invoke (Hy f) a = f (use a)

use :: b -> Hy a b
use = Hy Prelude.. const

func :: (a -> b) -> Hy a b
func f = Hy (\hy -> let b = f (invoke hy b) in b)


push :: (a -> b) -> (Hy a b -> Hy a b)
push f hab = Hy $ \(Hy ba) -> f $ ba hab


run :: Hy a a -> a
run (Hy aa_a) = aa_a Control.Category.id

instance Category Hy where
  id = fix $ push Prelude.id
  -- (.) :: Hy b c -> Hy a b -> Hy a c
  Hy cb_c . ab = Hy $ \ca -> cb_c (ab Control.Category.. ca)

-------------------------------------------------------------------------
data Tree a = a :+ [Tree a]


bfe ::  Tree a -> [[a]] -- outer list is a stream
bfe (a :+ below) = [a] : foldl (zipWith (++)) (repeat []) (bfe <$> below) -- [[2a], [], ...] : [[2b], [], ...] : [[2c], [3a], [], ...]
{-
  2a
1 2b
  2c 3a
-}

-- *Main> take 10 (bfe (1 :+ [2 :+ [], 3 :+ [], 4 :+ [5 :+ []]]))
-- [[1],[2,3,4],[5],[],[],[],[],[],[],[]]

-- back in the days this didn't fuse (build/fold rule), so people started looking for alternatives

main = print 1


foldEndo = foldr (Control.Category..) (Control.Category.id)





-- zip with hyperfunctions
{-
hzip :: forall a b . [a] -> [b] -> [(a, b)]
hzip xs ys = foldr xf xb xs (foldr yf yb ys)
  where xf :: a -> (fy -> [(a, b)]) -> (fy -> [(a, b)])
        xf = _
        xb :: fy -> [(a, b)]
        xb _ = []
        yf :: a -> (fx -> [(a, b)]) -> [(a, b)]
        yf = _
        yb _ _ = []
-}

-- this is best digested in hyperfunction way:
--    - code-reading supports intuition
--    - intuition supports code-reading

hzip :: forall a b. [a] -> [b] -> [(a, b)]
hzip xs ys = xz yz
  where
    -- hxz :: Hy (a -> [(a, b)]) [(a, b)]
    hxz@(Hy xz) = foldr f b xs
      where
        f x xk = Hy $ \(Hy yk) -> yk xk x
        b = Hy $ \_ -> []

    -- yz :: Hy [(a, b)] (a -> [(a, b)]) 
    yz = foldr f b ys
      where
        f y yk = Hy $ \(Hy xk) x -> (x, y) : xk yk
        b = Hy $ \_ _ -> []



-- bfe with hyperfunctions

hbfe :: Tree a -> [a]
hbfe = run Prelude.. f where
    -- f :: Tree a -> Hy [a] [a]
    f (a :+ ts) = push (a:) (foldEndo (f <$> ts))

{-
hbfe' :: Tree a -> [[a]]
hbfe' = map run Prelude.. run Prelude.. f where
    f :: Tree a -> Hy [Hy [a] [a]] [Hy [a] [a]]
    f (a :+ ts) = push (push (a:)) (_ $ foldEndo (f <$> ts))
-}

-- unification with hyperfunctions

data Ty = Int | Ar Ty Ty | Err deriving Show


type TyCh a = Hy a a



data Expr = Lit Int | Lam Expr | App Expr Expr


tych :: Expr -> (TyCh Ty -> TyCh Ty)
tych (Lit i) ch = push f ch
    where f Int = Int
          f _ = Err
tych (Lam e) ch = push (fst Prelude.. f) ( Control.Category.id  Control.Category.. tych e ch)
    where f (Ar _ co) = (Int, co)
          --f _ = (Err, _)

e0 = Lit 42

t0 = tych e0 Control.Category.id

ope.agda

{-# OPTIONS --guardedness #-}
open import Thrist


--        |   |   |   |  ...
--        \   |   /   |  ...
--         \  |  /    |  ...
--          \ | /     |  ...   ∞ x 1->1
--            op      |  ...   1 x 3->1 & ∞ x 1->1
--            |       |  ...
--            |       |  ...
--            |       |  ...   ∞ x 1->1

record Stream (A : Set) : Set where
  coinductive
  field
    hd : A
    tl : Stream A

open Stream

repeat : ∀ {A} → A → Stream A
hd (repeat x) = x
tl (repeat x) = repeat x


prepend : ∀ {A} → A → Stream A → Stream A
hd (prepend x _) = x
tl (prepend x xs) = xs

open import Data.List using (List; _∷_; []; [_])

prelist : ∀ {A} → List A → Stream A → Stream A
hd (prelist [] xs) = hd xs
hd (prelist (h ∷ _) _) = h
tl (prelist [] xs) = xs
tl (prelist (_ ∷ t) xs) = prelist t xs

module Test1 where
  import Relation.Binary.PropositionalEquality as Eq
  open Eq using (_≡_; refl; cong; sym)

  data Maybe (a : Set) : Set where
    nothing : Maybe a
    just : a -> Maybe a
  record _≈_ {A : Set} (xs ys : Stream A) : Set where
    coinductive
    field
      hd-≈ : hd xs ≡ hd ys
      tl-≈ : tl xs ≈ tl ys

  postulate lem-pre-repeat : ∀ {A} (x : A) -> prepend x (repeat x) ≡ repeat x
  open _≈_

  ≈-repeat : ∀ {A} (x : A) -> repeat x ≈ repeat x
  hd-≈ (≈-repeat x) = refl
  tl-≈ (≈-repeat x) = ≈-repeat x

  ≈-pre-repeat : ∀ {A} (x : A) -> prepend x (repeat x) ≈ repeat x
  hd-≈ (≈-pre-repeat x) = refl
  tl-≈ (≈-pre-repeat x) = ≈-repeat x


module Operations where
  data Op : ∀ {A : Set} (ins : List A) (out : A) -> Set where
    O0 : ∀ {A} (a : A) -> Op [] a
    O1 : ∀ {A} (a : A) -> Op [ a ] a
    Oµ : ∀ {A} (a b : A) -> Op (a ∷ b ∷ []) a
{-
  -- insert an Op into a ↓ b
  front-op : ∀ {A} {ins : List A} {out : A} {up down : Stream A}
           -> Op ins out -> up ↓ down
           -> prelist ins up ↓ prepend out down
  front-op (O0 a) updo = front [] a updo
  front-op (O1 a) updo = front [ a ] a updo
-}

  data _↑_↓_ {A} (op : List A -> A -> Set) : Stream A -> Stream A -> Set where
    done : ∀ (x : A) -> op ↑ repeat x ↓ repeat x
    oper : ∀ {xs ys} {xl} {y} -> op xl y -> op ↑ xs ↓ ys -> op ↑ prelist xl xs ↓ prepend y ys

  t5 : ∀ {A} {xs ys} (x : A) -> Op ↑ xs ↓ ys -> Op ↑ prelist [ x ] xs ↓ prepend x ys
  t5 x updo = oper (O1 x) updo

  t6 : ∀ {A} (x : A) -> Op ↑ prelist [ x ] (repeat x) ↓ prepend x (repeat x)
  t6 x = oper (O1 x) (done x)


module Capriotti where

  --          X
  --          ↓
  -- I ← A' → A → I

  P : Set₂
  P = ∀ {X : Set} {I : Set} → (X → I) → I → Set₁ where
  --  field
  --    A : 

  -- ops : P i j -> Set

PastingScheme.agda

-- Written by: András Kovács

data Con : Set
data Ty  : Con → Set
data Var : (Γ : Con) → Ty Γ → Set

data Con where
  ∙   : Con
  _▷_ : (Γ : Con) → Ty Γ → Con

data Ty where
  ★   : ∀ {Γ} → Ty Γ
  Ar  : ∀ {Γ}(A : Ty Γ) → Var Γ A → Var Γ A → Ty Γ

wk    : ∀ {Γ : Con} → (B : Ty Γ) → Ty Γ → Ty (Γ ▷ B)
wkVar : ∀ {Γ : Con} → (B : Ty Γ) → ∀ {A} → Var Γ A → Var (Γ ▷ B) (wk B A)

data Var where
  vz : ∀ {Γ : Con}{A : Ty Γ}   → Var (Γ ▷ A) (wk A A)
  vs : ∀ {Γ : Con}{A B : Ty Γ} → Var Γ A → Var (Γ ▷ B) (wk B A)

wk B ★          = ★
wk B (Ar A x y) = Ar (wk B A) (wkVar B x) (wkVar B y)

wkVar B vz                 = vs vz
wkVar B (vs {Γ} {A} {C} x) = vs {B = B} (wkVar C x)

-- Pasting schemes
--------------------------------------------------------------------------------

infixl 4 _▷_

data _⊢ : Con → Set
data _⊢_∋_ : (Γ : Con)(A : Ty Γ) → Var Γ A → Set

data _⊢ where
  stop : ∀ {Γ x} → Γ ⊢ ★ ∋ x → Γ ⊢

data _⊢_∋_ where
  sing : (∙ ▷ ★) ⊢ ★ ∋ vz
  ext  : ∀ {Γ A x} → Γ ⊢ A ∋ x → (Γ ▷ A ▷ Ar (wk A A) (wkVar A x) vz)
                                 ⊢ Ar (wk (Ar (wk A A) (wkVar A x) vz) (wk A A))
                                      (wkVar (Ar (wk A A) (wkVar A x) vz) (wkVar A x))
                                      (vs vz)
                                 ∋ vz

  down : ∀ {Γ A x y f} → Γ ⊢ Ar A x y ∋ f → Γ ⊢ A ∋ y

-- sc1 : _ ⊢
-- sc1 = stop (down (down (ext (ext sing))))

-- -- (∙ ▷ ★ ▷ ★ ▷ Ar ★ (vs vz) vz ▷ Ar ★ (vs (vs vz)) (vs vz)
-- --    ▷ Ar (Ar ★ (vs (vs (vs vz))) (vs (vs vz))) (vs vz) vz)

regensburg-2019-10-01.agda

{-# OPTIONS --guardedness #-}


import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)

data Nat : Set where
  Z : Nat
  S : Nat -> Nat

plus : Nat -> Nat -> Nat
plus Z n = n
plus (S m) n = S (plus m n)

zero-plus : ∀ {b} -> b ≡ plus b Z
zero-plus {Z} = refl
zero-plus {S b} = cong S zero-plus

zero-commutes : ∀ b -> plus Z b ≡ plus b Z
zero-commutes Z = refl
zero-commutes (S b) = cong S (zero-commutes b)

succ-commutes : ∀ a b -> S (plus b a) ≡ plus b (S a)
succ-commutes a Z = refl
succ-commutes a (S b) = cong S (succ-commutes a b)


plus-commutes : ∀ {a b} -> plus a b ≡ plus b a
plus-commutes {Z} {b}  = zero-commutes b
plus-commutes {S a} {b} rewrite plus-commutes {a} {b} = succ-commutes a b


plus-associates : ∀ {a b c} -> plus (plus a b) c ≡ plus a (plus b c)
plus-associates {Z} = refl
plus-associates {S a} {b} {c} rewrite plus-associates {a} {b} {c} = refl
-- plus-associates {S a} = cong S (plus-associates {a})








record Stream (A : Set) : Set where
  coinductive
  field
    hd : A
    tl : Stream A

open Stream



map : ∀ {A B} -> (A -> B) -> Stream A -> Stream B
hd (map f s) = f (hd s)
tl (map f s) = map f (tl s)




t1 : Stream Nat
hd t1 = Z
tl t1 = map S t1






repeat : ∀ {A} → A → Stream A
hd (repeat a) = a
tl (repeat a) = repeat a


prepend : ∀ {A} → A → Stream A → Stream A
hd (prepend x _) = x
tl (prepend _ xs) = xs

record _≅_ {A} (a : Stream A) (b : Stream A) : Set where
  coinductive
  field
    hd-≅ : hd a ≡ hd b
    tl-≅ : tl a ≅ tl b

open _≅_

≅-is-refl : ∀ {A} (a : Stream A) -> a ≅ a
hd-≅ (≅-is-refl a) = refl
tl-≅ (≅-is-refl a) = ≅-is-refl (tl a)

prep-≡ : ∀ {A} (a : A) -> prepend a (repeat a) ≅ repeat a
hd-≅ (prep-≡ a) = refl
tl-≅ (prep-≡ a) = ≅-is-refl (repeat a)

thrist.agda

module Thrist where

data Thrist {A : Set} (P : A -> A -> Set) : A -> A -> Set where
  nil : ∀ {a} -> Thrist P a a
  cons : ∀ {a b c} -> P a b -> Thrist P b c -> Thrist P a c


import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)

distill : ∀ {A} {from to : A} -> Thrist _≡_ from to -> from ≡ to
distill nil = refl
distill (cons refl as) rewrite distill as = refl

module Tests where

  import Add
  open Add
  t1 : ∀ a -> Thrist _≡_ (plus a Z) (plus a Z)
  t1 a = cons (lem-plus-z a) (cons (sym (lem-plus-z a)) nil)

  t2 : ∀ {a} -> Thrist _≡_ (plus a Z) (plus Z a)
  t2 {a} = cons (lem-plus-z a) (cons (refl) nil)