Skip to content

Instantly share code, notes, and snippets.

View andrewthad's full-sized avatar

Andrew Martin andrewthad

111 followers · 5 following
View GitHub Profile
@andrewthad
andrewthad / natural_join.hs
Created December 19, 2014 00:21
Haskell implementation of relational algebra's natural join
{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,
UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables #-}
import GHC.TypeLits
import Data.Type.Bool
import Data.Type.Equality
import Data.Proxy
import Control.Applicative ((<$>), (<*>))
import Data.Maybe (catMaybes)
@andrewthad
andrewthad / gist:563997cbc9d7d90cbc76
Created June 16, 2015 13:30
Yesod gitignore file
*.aux
cabal-dev
.cabal-sandbox
cabal.config
cabal.sandbox.config
*.chi
*.chs.h
config/client_session_key.aes
dist*
.DS_Store
@andrewthad
andrewthad / union.hs
Created December 27, 2015 22:27
Demonstration of GHC taking a long time to union two ordered type-level lists
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Proxy
@andrewthad
andrewthad / buffer-builder-no-orphan.hs
Created January 28, 2016 16:15
{-# LANGUAGE MagicHash #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.BufferBuilder.Aeson () where
import GHC.Base
import GHC.Integer.GMP.Internals
import Data.Aeson (Value (..))
import Data.BufferBuilder.Json (ToJson (..), nullValue, unsafeAppendBS, unsafeAppendUtf8Builder)
import qualified Data.BufferBuilder.Json as Json
@andrewthad
andrewthad / case_intersection.hs
Last active February 26, 2016 22:01
Case Intersection
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
main :: IO ()
main = putStrLn "hello"
@andrewthad
andrewthad / olist_broken.hs
Created July 7, 2016 21:22
{-# language DataKinds #-}
{-# language PolyKinds #-}
{-# language GADTs #-}
{-# language TypeOperators #-}
{-# language RankNTypes #-}
{-# language TypeFamilies #-}
{-# language TypeInType #-}
{-# language TypeFamilyDependencies #-}
{-# language UndecidableInstances #-}
@andrewthad
andrewthad / olist_working.hs
Created July 8, 2016 20:22
Type Level ordered list in haskell
{-# language DataKinds #-}
{-# language PolyKinds #-}
{-# language GADTs #-}
{-# language TypeOperators #-}
{-# language RankNTypes #-}
{-# language TypeFamilies #-}
{-# language TypeInType #-}
{-# language TypeFamilyDependencies #-}
{-# language UndecidableInstances #-}
@andrewthad
andrewthad / mutable_vectors_satisfying.hs
Created July 25, 2016 15:57
Failed attempt at added abstract predicate to mutable vectors
module Lib
( someFunc
) where
import Control.Monad.Primitive
import Data.Vector.Mutable (MVector,IOVector,unsafeNew,unsafeWrite)
import qualified Data.Vector.Mutable as MV
{-@ measure mvlen :: Data.Vector.MVector s a -> Int @-}
{-@ invariant { v : Data.Vector.MVector s a | 0 <= mvlen v } @-}
@andrewthad
andrewthad / mutable_vector_abstract_refinement.hs
Created July 26, 2016 12:20
module Lib
( someFunc
) where
import Control.Monad.Primitive
import Data.Vector.Mutable (MVector,IOVector,unsafeNew,unsafeWrite)
import qualified Data.Vector.Mutable as MV
{-@ measure mvlen :: Data.Vector.MVector s a -> Int @-}
{-@ invariant { v : Data.Vector.MVector s a | 0 <= mvlen v } @-}
@andrewthad
andrewthad / text_append_bench.hs
Created September 11, 2016 14:57
{-# OPTIONS -O2 -Wall #-}
module Main (main) where
import Criterion.Main
import Data.Text (Text)
import qualified Data.Text as Text
-- This benchmark demonstrates the non-linear performance of
-- appending text. The behavior I would expect would be that