andrewthad’s gists

andrewthad / dependent_haskell_quantifiers.markdown

Created October 16, 2017 13:35

Dependent Haskell Quantifiers

Quantifier	Dependency	Relevance	Visibility	Matchability
∀ (a :: τ ). ...	dep.	irrel.	inv. (unification)	unmatchable
∀ (a :: τ ) → ...	dep.	irrel.	vis.	unmatchable
Π (a :: τ ). ...	dep.	rel.	inv. (unification)	unmatchable
Π (a :: τ ) → ...	dep.	rel.	vis.	unmatchable
τ ⇒ ...	non-dep.	rel.	inv. (solving)	unmatchable
τ → ...	non-dep.	rel.	vis.	unmatchable

andrewthad / infinite_list_tree.hs

Created October 26, 2017 12:32

Variant of infinite tree that partition by evenness and oddness

	{-# language BangPatterns #-}

	import Prelude hiding (lookup)
	import Data.Primitive

	main :: IO ()
	main = do
	print $ lookup [17,15,6,999]

	data Tree a = Tree (Tree a) a (Tree a)

andrewthad / Arrs.hs

Created October 26, 2017 15:34

Fast Extensible Records

	{-# language PolyKinds #-}
	{-# language TypeOperators #-}
	{-# language LambdaCase #-}
	{-# language BangPatterns #-}
	{-# language KindSignatures #-}
	{-# language DataKinds #-}
	{-# language GADTs #-}
	{-# language RankNTypes #-}
	{-# language TypeFamilies #-}
	{-# language TypeFamilyDependencies #-}

andrewthad / hack_the_reader.hs

Created November 1, 2017 13:02

Benchmark queries in yesod

	instance YesodPersist App where
	type YesodPersistBackend App = SqlBackend
	runDB action = do
	master <- getYesod
	runSqlPool (hackTheReader action) $ appConnPool master

	newtype BenchmarkResults = BenchmarkResults [(Text,TimeSpec)]
	deriving Typeable
	type TypeMap = HashMap TypeRep Dynamic

andrewthad / sort_int_type.hs

Created November 9, 2017 13:06

Sort by converting to Nat

	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE UndecidableInstances #-}

	import GHC.TypeNats
	import Data.Kind (Type)

	main :: IO ()

andrewthad / unboxed_extensible_record_class.hs

Created November 9, 2017 15:02

Preliminary Implementation of Typeclasses for unboxed extensible records

	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE UndecidableInstances #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE FunctionalDependencies #-}
	{-# LANGUAGE MagicHash #-}
	{-# LANGUAGE TypeInType #-}
	{-# LANGUAGE GADTs #-}

andrewthad / extensible_typeclass_flattened.hs

Created November 9, 2017 15:58

Extensible record typeclass with better end-user interface

	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE UndecidableInstances #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE FunctionalDependencies #-}
	{-# LANGUAGE MagicHash #-}
	{-# LANGUAGE TypeInType #-}
	{-# LANGUAGE GADTs #-}

andrewthad / type_list_index.hs

Created November 9, 2017 19:33

Index into a type level list

	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE TypeApplications #-}
	{-# LANGUAGE AllowAmbiguousTypes #-}

andrewthad / unboxed_lambda.hs

Created November 16, 2017 16:39

The potential impact of functions with unboxed arguments

andrewthad / matrix_to_html.hs

Created November 20, 2017 19:23

Matrix to HTML

	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE ScopedTypeVariables #-}

	import qualified Data.Matrix as M
	import qualified Text.Blaze.Html5 as H
	import Text.Blaze.Html (Html,toHtml)
	import Text.Blaze.Renderer.Pretty (renderMarkup)

	main :: IO ()
	main = putStrLn (renderMarkup (matrixToHtml myMatrix))

Andrew Martin andrewthad