andrewthad’s gists

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 / 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 / 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 / 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 / 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 / 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 / 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 / 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 / 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 / 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

Andrew Martin andrewthad