This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DeriveFunctor #-} | |
{-# LANGUAGE DeriveGeneric #-} | |
{-# LANGUAGE DerivingStrategies #-} | |
{-# LANGUAGE DerivingVia #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE NoStarIsType #-} | |
{-# LANGUAGE PatternSynonyms #-} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE BangPatterns #-} | |
{-# LANGUAGE AllowAmbiguousTypes #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE DeriveAnyClass #-} | |
{-# LANGUAGE DeriveDataTypeable #-} | |
{-# LANGUAGE DeriveGeneric #-} | |
{-# LANGUAGE DerivingStrategies #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE GADTs #-} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{ | |
"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, |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DeriveFunctor #-} | |
{-# LANGUAGE DerivingStrategies #-} | |
{-# LANGUAGE DerivingVia #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE GeneralizedNewtypeDeriving #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE TupleSections #-} | |
{-# LANGUAGE TypeApplications #-} | |
{-# OPTIONS_GHC -Wno-orphans #-} |
NewerOlder