Skip to content

Instantly share code, notes, and snippets.

View cdepillabout's full-sized avatar

Dennis Gosnell cdepillabout

271 followers · 19 following
View GitHub Profile
@cdepillabout
cdepillabout / singleton-vec-proofs.hs
Created April 8, 2018 13:26
Using a structural type (type level Peano numbers) to try to simplify the replicateVec function.
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
@cdepillabout
cdepillabout / vec-proofs.hs
Created April 8, 2018 08:20
Writing replicateVec without needing the magic trick. A little simpler.
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
@cdepillabout
cdepillabout / cmpnat-proofs2.hs
Created April 8, 2018 08:17
Using a magic trick to prove laws about replicateVec
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
@cdepillabout
cdepillabout / weirderror.hs
Created April 7, 2018 16:21
weird compile error with proof for length indexed vector
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
@cdepillabout
cdepillabout / CmpNat-Proofs.hs
Last active April 8, 2018 13:31
sample of making and using proofs with CmpNat (and unsafeCoerce)
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
@cdepillabout
cdepillabout / extensible.hs
Created March 16, 2018 07:32
small example of hlist from extensible library
module Parser where
import Control.Applicative
-- this is from the extensible package
import Data.Extensible.HList
import Data.Text
-- the shape of the problem
--
-- we want a list of Parsers, all of different types.
@cdepillabout
cdepillabout / doubly-linked-list.hs
Created February 9, 2018 02:20
Doubly-linked list in Haskell, using MVars
{-# LANGUAGE NamedFieldPuns #-}
-- This is similar to https://gist.github.com/cblp/b427ffcce536d1a6b7e03598ec21e2ee
module Main where
import Control.Concurrent.MVar
import Control.Monad
import Data.List.NonEmpty
@cdepillabout
cdepillabout / example.hs
Last active August 25, 2017 15:29
non-lawful Monoid instances for building up AST considered not harmful in Haskell?
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
------------------------------------------------------
-- This is a gist for the stackoverflow question
-- https://stackoverflow.com/questions/45884762/non-lawful-monoid-instances-for-building-up-ast-considered-not-harmful-in-haskel
------------------------------------------------------
@cdepillabout
cdepillabout / lens-from-scratch.hs
Created August 4, 2017 13:17
Example of creating lenses in Haskell from scratch.
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE RankNTypes #-}
module Main where
import Data.Functor.Identity (Identity(Identity, runIdentity))
type Lens s a = forall f. Functor f => (a -> f a) -> s -> f s
data UserName = UserName { first :: String, second :: String } deriving Show
@cdepillabout
cdepillabout / small-lens-example.hs
Last active August 3, 2017 17:07
small example of using lens
#!/usr/bin/env stack
-- stack --resolver lts-9.0 script --package transformers --package lens -- -Wall
-- If you have stack installed, all you need to do is make this file executable
-- and you can run it from the command line.
module Main where
import Control.Lens (Prism', Traversal', _1, _2, preview, prism', set)