edsko

{-# 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

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

(* 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

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

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

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

-- | Lightweight checked exceptions

edsko

{-# 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

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

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

class Compare a b where

edsko

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

edsko

{-# 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

{-# 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