Andrew Miller amiller
amiller
/ gist:5095810
Created
March 6, 2013 00:50
This file contains hidden or 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 | |
| GADTs, FlexibleInstances, UndecidableInstances, | |
| StandaloneDeriving, DeriveFunctor, Rank2Types, | |
| GeneralizedNewtypeDeriving, ImpredicativeTypes | |
| #-} | |
| {- Andrew Miller | |
| Mendler style fixpoint, algebra, and fold | |
| See: Meta-Theory a la Carte | |
| http://www.cs.utexas.edu/users/bendy/papers/MTC.pdf |
This file contains hidden or 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
| {- | |
| Andrew Miller | |
| Authenticated Data Structures, Generically: | |
| Merkle-ized Lambda Calculator | |
| -} | |
| {-# LANGUAGE GADTs, | |
| FlexibleInstances, FlexibleContexts, UndecidableInstances, | |
| StandaloneDeriving, TypeOperators, Rank2Types, |
amiller
/ gist:5003106
Created
February 21, 2013 08:11
This file contains hidden or 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 | |
| GADTs, | |
| FlexibleInstances, FlexibleContexts, UndecidableInstances, | |
| StandaloneDeriving, TypeOperators, Rank2Types, | |
| MultiParamTypeClasses, ConstraintKinds, | |
| DeriveTraversable, DeriveFunctor, DeriveFoldable, | |
| TypeFamilies, FunctionalDependencies, | |
| ScopedTypeVariables, GeneralizedNewtypeDeriving | |
| #-} |
amiller
/ gist:5002697
Created
February 21, 2013 06:27
This file contains hidden or 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 | |
| GADTs, | |
| FlexibleInstances, FlexibleContexts, UndecidableInstances, | |
| StandaloneDeriving, TypeOperators, Rank2Types, | |
| MultiParamTypeClasses, | |
| DeriveTraversable, DeriveFunctor, DeriveFoldable, | |
| TypeFamilies, FunctionalDependencies, | |
| ScopedTypeVariables, GeneralizedNewtypeDeriving | |
| #-} | |
amiller
/ gist:5002022
Last active
December 14, 2015 00:49
This file contains hidden or 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 | |
| GADTs, | |
| FlexibleInstances, FlexibleContexts, UndecidableInstances, | |
| StandaloneDeriving, TypeOperators, Rank2Types, | |
| MultiParamTypeClasses, | |
| DeriveTraversable, DeriveFunctor, DeriveFoldable, | |
| TypeFamilies, FunctionalDependencies, | |
| ScopedTypeVariables, GeneralizedNewtypeDeriving | |
| #-} |
amiller
/ gist:4993375
Created
February 20, 2013 06:17
This file contains hidden or 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
| {- | |
| Andrew Miller - Feb 19 | |
| I'm playing around with indexed functors | |
| Generic Programming with Indexed Functors | |
| Andres Löh and Joseé Pedro Magalhães WGP 2012 | |
| http://www.dreixel.net/research/pdf/gpif.pdf |
amiller
/ gist:4989147
Created
February 19, 2013 19:42
This file contains hidden or 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
| {- | |
| Andrew Miller - RegTree.agda | |
| An attempt at translating "Exploring the Regular Tree Types" from Epigram | |
| http://strictlypositive.org/regular.pdf | |
| -} | |
| module RegTree where | |
| open import Data.Product |
amiller
/ gist:4715508
Last active
December 12, 2015 04:38
This file contains hidden or 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
| {- | |
| Andrew Miller | |
| Merkle Monads - Generalized Authenticated Data Structures in Haskell | |
| -} | |
| {-# LANGUAGE | |
| FlexibleInstances, FlexibleContexts, UndecidableInstances, | |
| StandaloneDeriving, TypeOperators, Rank2Types, |
amiller
/ gist:4659219
Last active
December 11, 2015 20:59
This file contains hidden or 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 | |
| FlexibleInstances, | |
| FlexibleContexts, | |
| UndecidableInstances, | |
| StandaloneDeriving, | |
| TypeOperators, | |
| UnicodeSyntax, | |
| Rank2Types, | |
| MultiParamTypeClasses, | |
| DeriveTraversable, DeriveFunctor, DeriveFoldable, |
amiller
/ gist:3940874
Created
October 23, 2012 19:03
This file contains hidden or 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
| (blockplayer)amiller@amiller-asus:~/projects/tahoe-lafs$ bin/tahoe debug trial allmydata.test.test_mutable.MultipleEncodings | |
| allmydata.test.test_mutable | |
| MultipleEncodings | |
| test_multiple_encodings ... [ERROR] | |
| =============================================================================== | |
| [ERROR] | |
| Traceback (most recent call last): | |
| Failure: twisted.trial.util.DirtyReactorAggregateError: Reactor was unclean. | |
| DelayedCalls: (set twisted.internet.base.DelayedCall.debug = True to debug) |