Skip to content

Instantly share code, notes, and snippets.

@cdepillabout
cdepillabout / doubly-linked-list.hs
Created Feb 9, 2018
Doubly-linked list in Haskell, using MVars
View doubly-linked-list.hs
{-# 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 Mar 16, 2018
small example of hlist from extensible library
View extensible.hs
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 Apr 8, 2018
sample of making and using proofs with CmpNat (and unsafeCoerce)
View CmpNat-Proofs.hs
{-# 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 Apr 7, 2018
weird compile error with proof for length indexed vector
View weirderror.hs
{-# 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 Apr 8, 2018
Using a magic trick to prove laws about replicateVec
View cmpnat-proofs2.hs
{-# 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 Apr 8, 2018
Writing replicateVec without needing the magic trick. A little simpler.
View vec-proofs.hs
{-# 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 Apr 8, 2018
Using a structural type (type level Peano numbers) to try to simplify the replicateVec function.
View singleton-vec-proofs.hs
{-# 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 Apr 8, 2018
Writing replicateVec without depending on the singleton library and without using structural typing.
View vec-proofs-no-singleton.hs
{-# 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 Apr 8, 2018
This file changes the plusMinusEq law to use Refl (:~:) instead of Dict.
View vec-proofs-using-refl-instead-of-dict.hs
{-# 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 Apr 12, 2018
Some notes for running `login-with` locally.
View play-with-login-with.md

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