Skip to content

Instantly share code, notes, and snippets.

@cdepillabout
cdepillabout / exists.md
Last active Nov 7, 2018
encode "exists" from classic logic in Haskell using singletons
View exists.md

I was reading through Type Theory and Formal Proofs (recommended by @parsonsmatt), and there was some info about how to represent "exists" (Ǝ).

In the type-theory version of classical logic, "exists" can represented as a higher-order function using "forall" like the following:

Ǝ x : S. P x is defined as ∀ A : *. (∀ x : S. P x -> A) -> A
@cdepillabout
cdepillabout / existential-vs-sigma.hs
Last active Jun 11, 2021
This file shows how similar existential types are vs. sigma types (dependent pairs).
View existential-vs-sigma.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
@cdepillabout
cdepillabout / vect-with-sigma.hs
Created Apr 14, 2018
Show how to use Sigma from singletons with type-indexed lists.
View vect-with-sigma.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
@cdepillabout
cdepillabout / magic2.hs
Created Apr 13, 2018
Example of how it is possible to override the functions that get called for a typeclass.
View magic2.hs
{-# 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
@cdepillabout
cdepillabout / magic1.hs
Created Apr 13, 2018
Example of running a function with a constraint of an instance that doesn't exist.
View magic1.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
-- | This module shows how it is possible to run a function with a constraint of
-- an instance that doesn't exist.
--
-- For instance, in the 'f' function, the 'Lala' 'Int' instance doesn't exist,
@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
@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 / 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 / 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.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 #-}