ncfavier

{-# LANGUAGE LambdaCase, BlockArguments, ViewPatterns #-}
import Data.MemoTrie

count :: [Int] -> Int
count = memoFix \ go -> \case
  [0, 0, 0, 0, 0] -> 1
  [a, b, c, d, e] -> sum $ [go [b, c, d, e, a - n] | n <- [1,3..a]]
                        <> [go [e, d, c, b, a - n] | n <- [2,4..a]]

main = print $ 2 * count (replicate 5 14)

ncfavier

function! s:unbackslash(str)
  return substitute(a:str, '\\\(.\)', '\1', 'g')
endfunction

" Parse a shell command line into a list of words, à la Perl's shellwords or
" Python's shlex.split.
function! s:shellwords(str)
  let l:args = []
  let l:len = len(a:str)
  let l:i = 0

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 ()