coefin.agda

module coefin.notarealagdafile where

-- This would be great syntax, but I don't think we can make it all implicit


------------------------------
-- Number/Numeral nonsense: --
------------------------------

-- `Fin` is an implicit coercion
Fin : Nat -> Type
Fin n = n

-- Likewise, `toℕ` is an implicit coercion
-- (the implicit variable may be tricky to deal with?)
toℕ : {n : Nat} -> Fin n -> ℕ
toℕ i = i

-- Implicit weakening?? Haven't thought much about it
weaken : {d n : Nat} -> Fin n -> Fin (d + n)
weaken i = i

-- Probably less useful in practice, but we need it to be transitive
FinFin : {n : Nat} -> Fin n -> Type
FinFin i = i

-- Would be great to have constructor overloading
zero : Nat
succ : Nat -> Nat
zero : {n : Nat} -> Fin (succ n)
succ : {n : Nat} -> Fin n -> Fin (succ n)

-- We want numerals to desugar to succ (… (succ zero))
0 : Nat
0 : {n : Nat} -> Fin (succ n)
1 : Nat
1 : {n : Nat} -> Fin (succ (succ n))
2 : Nat
..............

-- We want `(+)` to be overloaded
_+_ : Nat -> Nat -> Nat
zero + n = n
(succ d) + n = succ (d + n)

-- Why this shape? Because it is what we will use for indexing into concatenated
-- vectors
_↑+_ : (d : Nat) -> {n : Nat} -> Fin n -> Fin (d + n)
zero ↑+ n = n
(succ d) ↑+ n = succ (d ↑+ n)

-- We want it to be coherent with the coercions
toℕ (d ↑+ n) = d + toℕ n
-- ^ true by induction on `d`

-- However, what do we do about this?
data _⊕_ : Type -> Type -> Type where
  inl : {a b} -> a -> a ⊕ b
  inr : {a b} -> b -> a ⊕ b

-- This is clearly false
-- Fin (a + b) /= Fin a ⊕ Fin b

-- We could maybe get away with `Fin` computing on `succ` to something coherent
-- but I doubt it?
-- Fin (succ a) = Unit ⊕ Fin a
-- but Fin (succ zero) /= Unit

-- Maybe that is indication that we want `Fin` to remain explicit :(
-- So users choose how to partition finite types



-------------
-- Vectors --
-------------

Vec n a = Fin n -> a
-- but as a monomial, however we do that

[] : Vec 0 a
[_] : a -> Vec 1 a
[_, ..._] : a -> Vec n a -> Vec (succ n) a
[..._, _] : Vec n a -> a -> Vec (n + 1) a
[..._, ..._] : Vec n a -> Vec m a -> Vec (n + m) a

-- In general, we can come up with some arithmetic expression for the length
-- of a vector expression like this
-- And it means we can write case expressions very easily

[5, 6, 7, 8] 2 = 7

-- This is why we have ↑+
[...a, ...b] (length a ↑+ j) = b j
-- Why implicit weakening is good
[...a, ...b] (weaken i) = a i
-- Oh actually this is the wrong weaken, we need
weaken : {n d : Nat} -> Fin n -> Fin (n + d)
-- via commutativity n + d = d + n, bleh

-- To get around the coherence issues we can support sugar for sum elimination
[..._ | ..._] : (a -> r) -> (b -> r) -> (a ⊕ b) -> r
[5, 6 | 7, 8] (inr 0) = 7




-- aaanyways, this is just random thoughts on how we could make it more
-- ergonomic and approachable
--
-- I just wanted to skip straight to the fun part :D
--
-- maybe the 2ltt will help with some of these concerns? idk what it will look
-- like yet
--
-- regardless, it would be great to have some kind of row syntax so the burden
-- of keeping track of indices isn't foisted on numbers all the time