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

{-# 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 CPP                 #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

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

-- | Lightweight checked exceptions

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

edsko

import Control.Applicative
import Control.Monad
import Control.Monad.IO.Class
import System.IO.Unsafe

newtype LazyIO a = LazyIO { runLazyIO :: IO a }

instance Monad LazyIO where
  return a = LazyIO (return a)
  LazyIO x >>= f = LazyIO $ unsafeInterleaveIO $ x >>= runLazyIO . f

edsko

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

edsko

{-------------------------------------------------------------------------------
  Lazy n-ary cartesian product

  Most of these functions (except for 'cart' itself) are taken from
  "Generics.Deriving.Enum", which in turn are taken from Mark Jones' talk
  at AFP 2008.
-------------------------------------------------------------------------------}

-- | n-ary lazy cartesian product
ncart :: HList [] as -> [HList Identity as]

edsko

data Strategy = Concat

(+++) :: [a] -> [a] -> Strategy -> [a]
(+++) xs ys Concat = xs ++ ys

(.@) :: (Strategy -> a) -> Strategy -> a
(.@) = ($)

test :: [Int]
test = [1] +++ [2] .@ Concat

edsko

{-@ data List [listLen] a = Nil | Cons { hd :: a , tl :: List a } @-}
data List a = Nil | Cons a (List a)

{-@ measure listLen @-}
{-@ listLen :: List a -> Nat @-}
listLen :: List a -> Int
listLen Nil        = 0
listLen (Cons _ cs) = 1 + listLen cs