Rufflewind

import qualified Data.ByteString as B
import qualified Data.ByteString.Char8 as C

data Vec a = Vec { vecx, vecy, vecz :: !a }

instance Functor Vec where
   fmap f (Vec x y z) = Vec (f x) (f y) (f z)

instance Applicative Vec where
   pure x = Vec x x x

Rufflewind

-- Exercise: prove Peirce’s law <=> law of excluded middle in Haskell

{-# LANGUAGE Rank2Types #-}
module PeirceLEM where

import Data.Void

type Not a = a -> Void

type Peirce = forall a b. ((a -> b) -> a) -> a