Skip to content

Instantly share code, notes, and snippets.

gelisam / CategorySolver.agda
Created Apr 5, 2021
Automatically generating proofs which only involve associativity of composition and adding/removing identity morphisms.
View CategorySolver.agda
-- Yet another technique for generating proofs in Agda (in addition to the ones
-- I've described in
-- transform the proposition into a simpler one which can be proved using refl.
-- This is the approach I use in my
-- package, which can prove equations universally-quantified over finite types,
-- e.g. proving the commutativity of the boolean function '∧'. I simplify the
-- proposition to a long enumeration of all the concrete cases, each of which
-- can be proved using refl:
gelisam / StateRepl.hs
Created Mar 4, 2021
a ghci-like repl with State effects in addition to IO effects
View StateRepl.hs
-- In response to
-- The challenge is to write a repl in which we can run State effects in
-- addition to ghci's basic features of binding variables, inspecting values,
-- and running IO effects.
-- Well, the original request was whether it was possible to somehow add those
-- features to ghci. But being the maintainer of the hint library, I thought I
-- should demonstrate how easy it is to write your own ghci alternative which
-- has those features built-in!
gelisam / LensBenchmark.hs
Created Feb 12, 2021
benchmarking lens representations
View LensBenchmark.hs
-- inspired by this twitter conversation:
-- summary:
-- * by hand is fastest, then with a getter/setter pair, then van Laarhoven, then profunctor optics.
-- * in every representation, ghc can optimize 'view' to be as fast as doing it by hand
-- * there are no representations in which ghc can similarly optimize 'set' or 'modify'
-- criterion report:
{-# LANGUAGE RankNTypes, TupleSections #-}
gelisam / GeneratingCode.agda
Created Jan 11, 2021
Who says Agda doesn't have tactics? 4-ish mechanisms for generating proofs in Agda
View GeneratingCode.agda
-- A demonstration of Agda's mechanisms for generating proofs:
-- * 1. fromMaybe
-- * 2a. macros
-- * 2b. type-aware macros
-- * 2c. stuck macros
-- Tested using Agda- and agda-stdlib-1.4
module GeneratingCode where
gelisam / ActionSetOptics.hs
Created Nov 1, 2020
Representing optics by the set of actions they support.
View ActionSetOptics.hs
-- An alternative representation of optics.
-- I represent an optic as the set of actions it supports. Composition
-- intersects the sets, which is how e.g. composing a Lens with a Prism gives a
-- Traversal.
{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs, KindSignatures, MultiParamTypeClasses, RankNTypes, TypeFamilies, TypeOperators, UndecidableInstances #-}
{-# OPTIONS -Wno-name-shadowing #-}
module Main where
import Test.DocTest
gelisam / FreeBubbleSort.hs
Created Oct 15, 2020
optimizing bubble sort using free monads
View FreeBubbleSort.hs
-- In response to
-- and
-- The challenge is to implement bubble sort on lists... which makes no sense
-- at first glance, because bubble sort is defined in terms of swap operations,
-- which make little sense for lists!
{-# LANGUAGE DataKinds, FlexibleContexts, GADTs, MultiWayIf, QuantifiedConstraints, ScopedTypeVariables, TypeApplications, TypeOperators #-}
module Main where
import Test.DocTest
gelisam / ConfigurableMonadStack.hs
Created May 21, 2020
Using a runtime value to choose a monad transformer stack
View ConfigurableMonadStack.hs
-- in response to
-- We have a polymorphic action which can be instantiated to multiple
-- transformer stacks, and the goal is to use a runtime value to
-- determine which monad transformer stack to use.
{-# LANGUAGE AllowAmbiguousTypes, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, QuantifiedConstraints, RankNTypes, StandaloneDeriving, TypeApplications, UndecidableInstances #-}
{-# OPTIONS -Wno-orphans #-}
module Main where
import Test.DocTest
gelisam / AssociativeParser.hs
Last active May 19, 2020
prototype parser with an associative <|>
View AssociativeParser.hs
-- A prototype demonstrating a possible fix for
{-# LANGUAGE LambdaCase, TemplateHaskell #-}
{-# OPTIONS -Wno-name-shadowing #-}
module Main where
import Test.DocTest
import Control.Lens
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe
import Control.Monad.Reader
gelisam / ContextTransformers.hs
Last active Apr 24, 2020
deep pattern-matching in the finally-tagless style
View ContextTransformers.hs
-- How to convert an algorithm with deep pattern-matches into the
-- finally-tagless style in an extensible way; that is, in a way which makes it
-- possible to add a new constructor to the AST and corresponding cases to the
-- algorithm without modifying the code which has been written for the existing
-- constructors.
{-# LANGUAGE FlexibleInstances, LambdaCase, MultiParamTypeClasses #-}
module ContextTransformers where
import Test.DocTest
gelisam / DerivingViaSameShape.hs
Created Apr 23, 2020
using DerivingVia with types which are not representationally-equal
View DerivingViaSameShape.hs
-- DerivingVia is great when you want to delegate to a type which is
-- representationally-equal, in the sense that we can use coerce to convert
-- between the two types. But what if you want to delegate to a type which has
-- the same representation in the other sense of having the same shape? Here's a
-- trick!
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}