oisdk

primes : ∀ n → List (Fin n)
primes zero = []
primes (suc zero) = []
primes (suc (suc zero)) = []
primes (suc (suc (suc m))) = sieve (tabulate (just ∘ Fin.suc))
  where
  cross-off : ∀ {n} → Fin _ → Vec (Maybe _) n → Vec (Maybe _) n

  sieve : ∀ {n} →  Vec (Maybe (Fin (2 + m))) n → List (Fin (3 + m))
  sieve [] = []

oisdk

import Data.List (unfoldr, partition)
import Data.Maybe (catMaybes)
import Criterion.Main (defaultMain, env, bgroup, bench, nf)
import System.Random (randomIO)
import Control.Monad (replicateM)

groupOn :: Eq k => (a -> k) -> [a] -> [(k, [a])]
groupOn k = unfoldr f . map (\x -> (k x, x))
  where
    f [] = Nothing

oisdk

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveFunctor #-}

import Control.Applicative

data Free f a where
  Pure :: a -> Free f a
  App  :: f (a -> b) -> Free f a -> Free f b
  
instance Functor f =>  Functor (Free f) where

oisdk

{-# LANGUAGE BangPatterns    #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns, PatternSynonyms #-}
{-# LANGUAGE GeneralizedNewtypeDeriving, DerivingVia, DerivingStrategies #-}
{-# OPTIONS_GHC -Wall -fno-warn-name-shadowing #-}

import Data.Bits
import Data.Bool
import Test.QuickCheck hiding ((.&.))
import Control.Applicative

oisdk

{-# LANGUAGE RankNTypes #-}

import Control.Comonad.Cofree
import Control.Lens hiding ((:<))
import qualified Data.Map as Map
import Data.Map (Map)
import Prelude hiding (lookup)
import Data.Maybe (isJust)
import Test.QuickCheck

oisdk

---

title: Hyperfunctions, Breadth-First Traversals, and Search author: Oisín Kidney patat: theme: codeBlock: [vividBlack] code: [vividBlack] incrementalLists: true eval: ruby:

oisdk

{-# LANGUAGE GADTs, DataKinds, TypeOperators, FlexibleInstances, KindSignatures, RankNTypes, QuantifiedConstraints, FlexibleContexts #-}

data Free (fs :: [(* -> *) -> * -> *]) (a :: *) where
  Pure   :: a -> Free '[] a
  Effect :: f (Free fs) a -> Free (f ': fs) a
  
instance Functor (Free '[]) where
  fmap f (Pure x) = Pure (f x)
  
instance ((forall x. Functor x => Functor (f x))

oisdk

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

module ReductionProblem where

open import Agda.Builtin.Nat using (Nat; suc; zero)
open import Agda.Primitive using (_⊔_)
open import Agda.Builtin.Equality using (_≡_; refl)

-- The Acc type, defined as a record:
record Acc {a r} {A : Set a} (R : A → A → Set r) (x : A) : Set (a ⊔ r) where

oisdk

{-# LANGUAGE UnicodeSyntax        #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import Data.Functor.Const

oisdk

-- Selective lets us do "monadic" binds where the domain is restricted
-- to the countable types (which can be infinite).

{-# LANGUAGE TypeOperators     #-}
{-# LANGUAGE PatternSynonyms   #-}
{-# LANGUAGE ViewPatterns      #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts  #-}

import GHC.Generics