Lysxia

import Control.Applicative
import Control.Monad

-- Examples

example1 :: M r String ()
example1 = do
  newError "expected True"
  True <- bad
  pure ()

Lysxia

module I where

open import Data.Unit
open import Relation.Binary.PropositionalEquality

private variable
  A : Set

to : (⊤ → A) → A
to f = f tt

Lysxia

{-# LANGUAGE
  DataKinds,
  DeriveGeneric,
  PolyKinds,
  StandaloneDeriving,
  TypeFamilies,
  UndecidableInstances #-}
module T where

import Data.Kind (Constraint, Type)

Lysxia

{-# OPTIONS --without-K #-}
module C where

open import Function
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; trans; cong; sym)
open import Data.Empty
open import Data.Bool
open import Data.Product as Prod using (∃-syntax; Σ-syntax; _,_; _×_; ∃; proj₁; proj₂)
open import Data.Maybe as Maybe using (Maybe; just; nothing; is-just)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)

Lysxia

{-# LANGUAGE GADTs #-}
module Main where

import Control.Applicative (liftA2)

data Yaml
  = String String
  | Object [(String, Yaml)]
  deriving Show

Lysxia

-- Implementing weight-balanced trees using recursion schemes.
-- (actually just concat3 from Adams's report)
-- https://stackoverflow.com/questions/74651343/using-a-paramorphism-inside-of-an-apomorphism
--
-- References for WBT:
-- - Implementing Sets Efficiently in a Functional Language, Stephen Adams, 1992
--   https://ia600700.us.archive.org/0/items/djoyner-papers/SHA256E-s234215--592b97774eca4193a05ed9472ab6e23788d3a0bea5d1b98cef301460ab4010ee.pdf
-- - Binary search trees of bounded balance, J. Nievergelt and E. M. Reingold
--   https://dl.acm.org/doi/10.1145/800152.804906
-- - Balancing Weight-Balanced Trees, Y. Hirai and K. Yamamoto

Lysxia

-- | Ordered affine spaces are made of points and vectors.
--
-- - Vectors can be added, that's the 'Semigroup' superclass.
-- - Points can be translated along vectors using @('.+')@.
-- - Given two ordered points @i <= j@, @j '.-.?' i@ finds a vector @n@
--   such that @i + n = j@.
--
-- In other words, we only require the existence of "positive" vectors.
--
-- __Laws:__

Lysxia

{-# LANGUAGE OverloadedStrings, DerivingVia, LambdaCase, FunctionalDependencies, MultiParamTypeClasses #-}
module W where

import Control.Monad.Trans.Free
import Control.Monad.Writer
import Control.Applicative
import Data.Functor.Classes (Eq1(..))
import Data.Text (Text)
import qualified Data.Text as T

Lysxia

-- 1. Prove X⁷≡X in the polynomial quotient semiring ℕ[X]/(X≡X²+1)
-- 2. Define a map toType : ℕ[X]/(X≡X²+1) → Type,
--    using the semiring structure of Type and the fact that
--    the equation T≡T²+1 holds for the type of binary trees T.
-- 3. We deduce T⁷ ≡ T, by T⁷ ≡ toType X⁷ ≡ toType X ≡ T
-- 4. ???
-- 5. Profit

{-# OPTIONS --cubical #-}
module S where

Lysxia

{-# OPTIONS --cubical #-}
module S where

open import Cubical.Core.Everything
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport