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