Skip to content

Instantly share code, notes, and snippets.

View TOTBWF's full-sized avatar

Reed Mullanix TOTBWF

View GitHub Profile
@TOTBWF
TOTBWF / profuck.pl
Last active September 25, 2017 20:09
BrainFuck in Prolog
:- set_prolog_flag(double_quotes, chars).
tape(N, List) :- length(List, N), zeros(List).
zeros([]).
zeros([0|T]) :- zeros(T).
interpret(_, [], _, _, _, Acc) --> { reverse(Acc, RAcc) }, RAcc.
interpret(Seen, [+|Next], Left, [Data], Right, Acc) --> { NData is Data + 1}, interpret([+|Seen], Next, Left, [NData], Right, Acc).
interpret(Seen, [-|Next], Left, [Data], Right, Acc) --> { NData is Data - 1}, interpret([-|Seen], Next, Left, [NData], Right, Acc).
@TOTBWF
TOTBWF / Traversable.hs
Created September 3, 2018 03:33
A possible implementation of mapAccumLM and mapAccumRM
newtype StateLT s m a = StateLT { runStateLT :: s -> m (s,a) }
instance (Functor m) => Functor (StateLT s m) where
fmap f (StateLT k) = StateLT $ \s -> fmap (\(s',a) -> (s', f a)) $ k s
instance Monad m => Applicative (StateLT s m) where
pure a = StateLT $ \s -> return (s, a)
StateLT kf <*> StateLT kv = StateLT $ \s -> do
(s', f) <- kf s
(s'', v) <- kv s'
{-
Requires (from Stack lts-12.11)
- arithmoi >= 0 && < 1
- containers >= 0.5 && < 0.6
- parallel >= 3 && < 4
- split >= 0.2 && < 0.3
-}
import qualified Math.NumberTheory.Primes.Sieve as Math
import Data.IntSet (IntSet)
@TOTBWF
TOTBWF / Santa.hs
Last active November 29, 2018 21:21
import Control.Monad (zipWithM)
import Data.Foldable (foldlM)
data Command = Up | Down
parseChar :: Char -> Int -> Either String Command
parseChar '(' _ = Right Up
parseChar ')' _ = Right Down
parseChar c i = Left $ "Parse Error: unexpected token " ++ [c] ++ " at index " ++ (show i)
@TOTBWF
TOTBWF / MTLDerivingVia.hs
Last active November 6, 2021 16:59
Deriving MTL classes using -XDerivingVia
-- |
-- Module : Lift
-- Copyright : (c) Reed Mullanix 2019
-- License : BSD-style
-- Maintainer : reedmullanix@gmail.com
--
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
@TOTBWF
TOTBWF / Cayley.agda
Created July 12, 2019 22:02
Cayleys Theorem in Agda
{-# OPTIONS --without-K --safe #-}
open import Algebra
module Cayley {a ℓ} {S : Semigroup a ℓ} where
open Semigroup S renaming (Carrier to A; assoc to ∙-assoc; setoid to S-Setoid )
open import Algebra.Structures
open import Algebra.Morphism; open Definitions
@TOTBWF
TOTBWF / HProfunctor.hs
Created September 23, 2019 22:25
Higher Profunctors
type (~>) f g = forall x. f x -> g x
class HProfunctor (p :: (* -> *) -> (* -> *) -> * -> *) where
hdimap :: (f ~> g) -> (h ~> i) -> p g h ~> p f i
instance HProfunctor Ran where
hdimap fg hi r = Ran $ \k -> hi $ runRan r (fg . k)
instance HProfunctor Lan where
hdimap fg hi (Lan gbx h) = Lan (gbx . fg) (hi h)
@TOTBWF
TOTBWF / Pullback.hs
Created May 14, 2020 01:08
Pullbacks in (dependent) haskell
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE GADTs #-}
module Pullbacks where
@TOTBWF
TOTBWF / TypeFamilyDrama.hs
Created August 21, 2020 01:32
A weird case where destructuring a tuple causes type errors
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
module Lib where
import Data.Functor.Const
type family NonInjective env a = result | result -> env where
NonInjective env (a -> r) = [env] -> NonInjective env r
NonInjective env a = [env]
@TOTBWF
TOTBWF / HigherCategories.agda
Created August 23, 2020 07:11
Some stuff from "Higher Operads, Higher Categories"
{-# OPTIONS --without-K --safe #-}
-- Some stuff from "Higher Operads, Higher Categories"
-- https://arxiv.org/abs/math/0305049
module MultiCategory where
open import Level
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry)
open import Categories.Category
open import Categories.Bicategory