Skip to content

Instantly share code, notes, and snippets.

View aljce's full-sized avatar

Alice McKean aljce

  • Portland, OR
View GitHub Profile
@aljce
aljce / lexer.rs
Created September 11, 2016 23:13
struct Group<'a> {
name: &'a str,
groups: Vec<&'a str>
}
fn is_whitespace(c: char) -> bool {
c == ' ' || c == '\t' || c == '\n'
}
fn isnt_whitespace(c: char) -> bool {
@aljce
aljce / mtl.hs
Last active September 25, 2016 16:28
{-# LANGUAGE MultiParamTypeClasses,
FunctionalDependencies,
FlexibleInstances #-} --Three extensions compared to just type families
{-# LANGUAGE TypeFamilies #-}
module Mtl where
newtype ReaderT r m a = ReaderT { unReaderT :: r -> m a }
instance (Functor m) => Functor (ReaderT r m) where
fmap f (ReaderT x) = ReaderT (\k -> fmap f (x k))
let
pkgs = import <nixpkgs> {};
stdenv = pkgs.stdenv;
top-level = import ./top-level.nix { haskellPackages = pkgs.haskellPackages;
dontCheck = pkgs.haskell.lib.dontCheck;
testTopLevel = false; };
in {
haskellEnv = stdenv.mkDerivation {
name = "haskell-env";
version = "1.1.1.1";
let pkgs = import <nixpkgs> { };
top-level = import ./top-level.nix { haskellPackages = pkgs.haskellPackages;
dontCheck = pkgs.haskell.lib.dontCheck;
cabal-install = pkgs.cabal-install;
testTopLevel = false; };
in
{ haskell-env = pkgs.stdenv.mkDerivation {
name = "haskell-env";
buildInputs = [ pkgs.cabal-install top-level.frank.env ];
};
module Id where
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
sym : ∀ {A} {x y : A} -> x ≡ y -> y ≡ x
sym refl = refl
_qed : ∀ {A} -> (x : A) -> x ≡ x
_ qed = refl
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
module Simple where
import Data.Kind (Type)
@aljce
aljce / Monad.agda
Last active September 18, 2017 04:10
module Monad where
open import Data.Nat
open import Data.Vec hiding (_>>=_)
record Monad (m : Set -> Set) : Set₁ where
infixl 1 _>>=_
field
pure : ∀ {a : Set} -> a -> m a
_>>=_ : ∀ {a b : Set} -> m a -> (a -> m b) -> m b
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}
module Unsafe.Maybe where
import GHC.Prim (Addr#,nullAddr#,addrToAny#,anyToAddr#,eqAddr#,unsafeCoerce#)
import GHC.Magic (runRW#)
import GHC.Types (Any)
import Unsafe.Coerce (unsafeCoerce)
module Chapter2 where
open import Agda.Builtin.FromNat
open import Data.Nat using (ℕ; zero; suc)
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.Core using (Decidable)
open import Relation.Binary.PropositionalEquality
@aljce
aljce / Co.agda
Last active December 21, 2017 02:10
module Co where
open import Level hiding (suc)
open import Size
open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Nat hiding (_⊔_)
open import Data.Vec using (Vec ; [] ; _∷_)
open import Data.List using (List ; [] ; _∷_)