Skip to content

Instantly share code, notes, and snippets.

View isovector's full-sized avatar

Sandy Maguire isovector

View GitHub Profile
module adders where
open import Relation.Binary.PropositionalEquality
using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning; _≗_)
open import Function
using (_∘_; id)
private variable
A B C D X Y Z W : Set
f f₁ f₂ g₁ g₂ t t₁ t₂ b b₁ b₂ l l₁ l₂ r r₁ r₂ : A → B
@isovector
isovector / Copatterns.agda
Created January 29, 2022 19:39
Review: Copatterns
{-# OPTIONS --guardedness --type-in-type #-}
module Copatterns where
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
open Relation.Binary.PropositionalEquality.≡-Reasoning
data Nat : Set where
zero : Nat
suc : Nat -> Nat
@isovector
isovector / Clowns.hs
Created January 23, 2022 21:47
blog post: review of clowns and jokers
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PatternSynonyms #-}
Jonathan:
My thought process was that like, "Everybody's doing the same
thing. Everybody's reading Cracking the Coding Interview.
Everybody's reading books, doing Udemy courses, what is something
different that I can do to accelerate myself?"
Sandy:
Hello and welcome to the very first episode of the Cofree Cast.
I'm your host, Sandy Maguire, and today, I'm joined by Jonathan
Lorimer. Jonathan is a software developer based in Toronto, who's
import qualified Data.Set as S
import Data.Set (Set)
import Data.Char (isLower)
import Data.Ord (comparing, Down (Down))
import Data.List (sortBy, subsequences, minimumBy, maximumBy)
import Control.Monad.Trans.Writer.CPS
import Data.Monoid
import Data.Foldable (traverse_)
wordFilter :: String -> Bool
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
prepropEquivInterpreters
:: forall effs x r1 r2
. (Eq x, Show x, Inject effs r1, Inject effs r2, Members effs effs)
=> (forall a. Sem r1 a -> IO a)
-> (forall a. Sem r2 a -> IO a)
-> (forall r. Members effs r => Gen (Sem r x))
-> Property
prepropEquivInterpreters int1 int2 mksem = property $ do
SomeSem sem <- liftGen @effs @x mksem
pure $ ioProperty $ do
{
"haskell.serverExecutablePath": "/home/sandy/prj/hls/.stack-work/install/x86_64-linux-tinfo6/95210f202fcc608b16b9b498dd9af8f1b8d43ff153fe428a250346ccc0cf33e5/8.8.4/bin/haskell-language-server",
"haskell.formatOnImportOn": false,
"haskell.plugin.tactics.config.features": "QrfgehpgNyy/HfrQngnPba/ErsvarUbyr/XabjaZbabvq/RzcglPnfr/QrfgehpgCha/Zrgncebtenz",
"window.zoomLevel": 1,
"files.exclude": {
"**/.git": true,
"**/.svn": true,
"**/.hg": true,
"**/CVS": true,
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
-- typechecking goes really fast if you uncomment this line
-- {-# OPTIONS_GHC -fmax-valid-hole-fits=0 #-}
module SlowTypecheck where
import HsExpr
@isovector
isovector / StateChart.hs
Last active May 9, 2021 20:20
statechart2.hs
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-orphans #-}