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

{-# 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

{-# 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

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

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

{-# 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

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

ncfavier

    canonical-elements⇒type-like : is-set Carrier → canonical-elements → type-like c
    canonical-elements⇒type-like set
      record { canon = canon
             ; canon-≈ = canon-≈
             ; canon-≡ = canon-≡ }
      =
      record { type-like-to = Σ _ λ a → canon a ≡ a
             ; type-like-≅ = record { iso = record { _⟨$⟩_ = λ a → canon a , canon-≡ _ _ (canon-≈ a)
                                                   ; cong = λ s → Σ-≡ (canon-≡ _ _ s) set }
                                    ; inv = record { _⟨$⟩_ = fst

ncfavier

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

ncfavier

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