Skip to content

Instantly share code, notes, and snippets.

View cdepillabout's full-sized avatar

Dennis Gosnell cdepillabout

272 followers · 19 following
View GitHub Profile
@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 / 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-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 / 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-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 / vec-proofs-using-refl-instead-of-dict.hs
Created April 8, 2018 23:31
This file changes the plusMinusEq law to use Refl (:~:) instead of Dict.
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
@cdepillabout
cdepillabout / vec-proofs-no-singleton.hs
Created April 8, 2018 15:36
Writing replicateVec without depending on the singleton library and without using structural typing.
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
@cdepillabout
cdepillabout / play-with-login-with.md
Last active April 12, 2018 08:13
Some notes for running `login-with` locally.

Here are some notes for playing around with login-with locally.

login-with assumes that it will be accessed over https. Since we are just playing around with it, we want to run it locally. We don't want to mess with setting up nginx as a reverse proxy.

We can use socat as a quick reverse proxy.

First, we need to create a certificate socat can use. (Ideally, socat would create a certificate for us every time it runs, but it doesn't look like that functionality exists...) openssl is used to create the ceritificate:

$ openssl req -new -x509 -days 365 -nodes -out cert.pem -keyout cert.key
@cdepillabout
cdepillabout / magic2.hs
Created April 13, 2018 16:30
Example of how it is possible to override the functions that get called for a typeclass.
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
-- | This modules shows how it is possible to override the functions that get
-- called for a typeclass.
--
-- For instance, the 'foo' function overrides the '(<>)' function for