ncfavier

module wip.Delay where
open import 1Lab.Prelude
open import Data.Sum
open import Data.Nat

private variable
  ℓ : Level
  A B : Type ℓ

record Delay {ℓ} (A : Type ℓ) : Type ℓ where

ncfavier

{-# LANGUAGE UnicodeSyntax #-}

-- n-ary functions s^n → a.
-- N s is the free Applicative on Reader s.
-- It encodes the effect "ask for one s", but since it's an Applicative
-- and not a Monad you can statically know how many arguments a function requires.
data N s a = Pure a | Ask (N s (s → a))

arity :: N s a → Integer
arity (Pure _) = 0

ncfavier

{-# LANGUAGE MagicHash, UnboxedTuples #-}
import GHC.Prim
import Unsafe.Coerce
import Prelude hiding (id)

main :: IO ()
main = do
  print (id True)
  print (id False)
  print (id 15)

ncfavier

{-# OPTIONS --without-K #-}

open import Agda.Primitive

private variable
  ℓ ℓ' : Level
  A B : Set ℓ

data _≡_ {A : Set ℓ} : A → A → Set ℓ where
  refl : {a : A} → a ≡ a

ncfavier

open import Agda.Primitive renaming (Set to Type)
open import Data.Product
open import Relation.Binary.PropositionalEquality

Futamura projections

Let us represent programs from inputs I to outputs O as simple functions I → O, and assume we have a specialiser: a program that partially evaluates another program applied to the "static" part of its input.

ncfavier

-- Moved to https://agda.monade.li/NatChurchMonoid.html

ncfavier

{ size ? 1000 }: with builtins;
let
  enumerate = genList (i: i + 1);
  sum = foldl' add 0;
  divides = n: k: n / k * k == n;
  factors = n: filter (divides n) (enumerate (n / 2));
  perfect = n: sum (factors n) == n;
in
filter perfect (enumerate size)

ncfavier

module LEM where

open import 1Lab.Type
open import 1Lab.Path
open import 1Lab.HLevel
open import 1Lab.HIT.Truncation
open import Data.Sum

⊥-is-prop : is-prop ⊥
⊥-is-prop ()

ncfavier

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

open import Cubical.Foundations.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary

data ℤ : Type where

ncfavier

open import 1Lab.Type
open import 1Lab.Path
open import 1Lab.Path.Groupoid
open import Data.Bool

data Niltok : Type where
  t : Niltok
  nicht : Niltok → Niltok
  mod2 : (n : Niltok) → n ≡ nicht (nicht n)
  coh : (n : Niltok) → ap nicht (mod2 n) ≡ mod2 (nicht n)