Skip to content

Instantly share code, notes, and snippets.

Avatar

Donnacha Oisín Kidney oisdk

View GitHub Profile
View bft-hyperfunction-presentation.markdown

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

View effects.hs
{-# 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))
View ReductionProblem.agda
{-# 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
View container.hs
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind
import Data.Functor.Const
View selective-countable.hs
-- 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
View taba.hs
{-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds, RankNTypes, ScopedTypeVariables, TypeOperators #-}
import Data.Kind
import Data.Coerce
data Nat = Z | S Nat
data Vec (a :: Type) (n :: Nat) where
Nil :: Vec a Z
(:-) :: a -> Vec a n -> Vec a (S n)
View catalan.hs
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveFoldable, DeriveTraversable, DeriveFunctor #-}
import Data.List (mapAccumL)
data Stream a = a :< Stream a deriving (Functor, Foldable, Traversable)
infixr 5 :<
instance Show a => Show (Stream a) where
showsPrec n = showsPrec n . foldr (:) []
View brauntolist.hs
import Test.QuickCheck
import Data.Tree.Binary.Preorder (Tree(..), drawTree)
import Control.Arrow (first)
import Data.List (unfoldr)
fromList :: [a] -> Tree a
fromList xs = head (l (foldr f b xs 1 2))
where
b _ _ ys zs = (repeat Leaf, (repeat Leaf, ys))
View ids.hs
{-# LANGUAGE DeriveFunctor, LambdaCase, BlockArguments, BangPatterns, RankNTypes, GeneralisedNewtypeDeriving, OverloadedLists, TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
import Control.Monad
import Control.Applicative
import Numeric.Natural
import GHC.Exts
import GHC.Base (build)
View matrix.hs
{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, NoStarIsType #-}
{-# OPTIONS_GHC -Wall -fno-warn-unticked-promoted-constructors #-}
import Data.Monoid (Sum(..))
import Data.Kind (Type)
data Nat = Z | S Nat
data Fin (n :: Nat) where