TOTBWF

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module ObfuscatedSKI where

import Unsafe.Coerce (unsafeCoerce)

--------------------------------------------------------------------------------
-- A Lambda to SKI Combinator Compiler, written entirely using SKI Combinators
--

TOTBWF

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module IOHCC where

import Unsafe.Coerce

u = unsafeCoerce

TOTBWF

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}

TOTBWF

module DayOne where

-- Lets build this up from scratch, for didactic purposes.
-- If we were doing this "for real" we ought to use agda-stdlib.

--------------------------------------------------------------------------------
-- Basic Definitions
--------------------------------------------------------------------------------

-- First, natural numbers and lists. Nothing too exciting here.

TOTBWF

-- A proof of the Knaster-Tarski Fixpoint Theorem
-- See https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem
module Fixpoint where

open import Level
open import Data.Product

open import Relation.Binary
open import Relation.Binary.Morphism

TOTBWF

-- Regexes via Brzozowski derivatives
{-# OPTIONS --without-K --safe #-}
module Regex where

open import Function

open import Data.Char
open import Data.Char.Properties renaming (_≟_ to _≟ᶜ_)
open import Data.String using (toList)
open import Data.Bool

TOTBWF

{-# OPTIONS --without-K --safe #-}
-- Some stuff from "Higher Operads, Higher Categories"
-- https://arxiv.org/abs/math/0305049
module MultiCategory where

open import Level
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry)

open import Categories.Category
open import Categories.Bicategory

TOTBWF

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
module Lib where

import Data.Functor.Const

type family NonInjective env a = result | result -> env where
    NonInjective env (a -> r) = [env] -> NonInjective env r
    NonInjective env a        = [env]

TOTBWF

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE GADTs #-}
module Pullbacks where

TOTBWF

type (~>) f g = forall x. f x -> g x

class HProfunctor (p :: (* -> *) -> (* -> *) -> * -> *) where
  hdimap :: (f ~> g) -> (h ~> i) -> p g h ~> p f i

instance HProfunctor Ran where
  hdimap fg hi r = Ran $ \k -> hi $ runRan r (fg . k)

instance HProfunctor Lan where
  hdimap fg hi (Lan gbx h) = Lan (gbx . fg) (hi h)