edsko’s gists

edsko / QQAST.hs

Last active March 3, 2024 00:39

See http://www.well-typed.com/blog/2014/10/quasi-quoting-dsls/ .

	{-# LANGUAGE DeriveDataTypeable, GeneralizedNewtypeDeriving, TemplateHaskell, FlexibleInstances #-}
	{-# OPTIONS_GHC -Wall -fno-warn-missing-signatures #-}
	module QQAST where

	import Control.Applicative
	import Control.Exception
	import Control.Monad.State
	import Data.Data (Data)
	import Data.Generics (extQ)
	import Data.IORef

edsko / Lenses.hs

Last active August 29, 2015 14:16

Proof of equivalence for van Laarhoven lenses

	-- Example from http://arxiv.org/pdf/1103.2841v1.pdf
	-- "Functor is to Lens as Applicative is to Biplate"

	-- NOTE: Proof of equivalence here _IMPLIES_ proof of equivalence for
	-- van Laarhoven lenses (Section 4)

	{-# OPTIONS_GHC -Wall #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE RecordWildCards #-}

edsko / parametricity.coq

Last active January 23, 2020 20:31

Formalization of a small part of the Parametricity Tutorial blog post

	(* Developed using Coq 8.4pl5 *)

	Require Import Coq.Setoids.Setoid.
	Require Import Coq.Logic.ProofIrrelevance.
	Require Import Coq.Logic.JMeq.

	Set Implicit Arguments.

	(* Auxiliary *)

edsko / callbacks.hs

Last active January 14, 2019 06:43

Alleviating callback hell in Haskell

	{-------------------------------------------------------------------------------
	Discussion of ContT in terms of callbacks

	For an alternative exposition, see
	<http://www.haskellforall.com/2012/12/the-continuation-monad.html>.
	-------------------------------------------------------------------------------}

	{-# OPTIONS_GHC -Wall #-}

	import Control.Exception

edsko / Checked.hs

Last active October 26, 2016 19:15

Lightweight checked exceptions in Haskell

	{-# LANGUAGE CPP #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE ScopedTypeVariables #-}

	#if __GLASGOW_HASKELL__ >= 710
	{-# LANGUAGE AllowAmbiguousTypes #-}
	#endif

	-- \| Lightweight checked exceptions

edsko / CheckedRevisited.hs

Last active November 3, 2021 08:35

Lightweight checked exceptions in Haskell without `unsafeCoerce`

	{-# OPTIONS_GHC -Wall -fno-warn-unused-binds #-}
	{-# LANGUAGE CPP #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE IncoherentInstances #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE ScopedTypeVariables #-}

	#if __GLASGOW_HASKELL__ >= 708
	{-# LANGUAGE RoleAnnotations #-}
	#endif

edsko / Overlapping.hs

Created September 24, 2015 12:39

Incoherence using only overlapping instances and existentials, and avoiding it using a type family

	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE TypeOperators #-}

	import Prelude hiding (compare)
	import Data.Type.Equality

	class Compare a b where

edsko / DependentServant.hs

Last active July 2, 2020 06:52

See "Dependently typed servers in Servant" (http://www.well-typed.com/blog/2015/12/dependently-typed-servers/) for the blog post accompanying this gist.

	{-# LANGUAGE ConstraintKinds #-}
	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE KindSignatures #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE OverloadedStrings #-}
	{-# LANGUAGE RankNTypes #-}

edsko / LiftImplies.hs

Last active February 23, 2017 17:08

	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE KindSignatures #-}
	{-# LANGUAGE StaticPointers #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE UndecidableInstances #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE ConstraintKinds #-}
	{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}

edsko / Defunctionalization.hs

Last active May 19, 2017 08:00

Using defunctionalization to avoid partially applied type synonyms

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE KindSignatures #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE PolyKinds #-}

	data Fn a = Id \| Const a

	type family Apply (fn :: Fn k) (a :: k) :: k where
	Apply Id a = a
	Apply (Const b) a = b

Edsko de Vries edsko