Answer to a question at our Intersections KW Meetup: http://www.meetup.com/Intersections-KW/events/221476419/

not.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Foo where

import Prelude hiding (Bool(..), not)

-- | at Intersections KW #8 a very good question was asked. After
-- writing the `Not` type family below and showing how a bad `not`
-- function would be impossible, Steven asked:
--
-- "haven't you just moved the error to the type level? How do you
-- prevent yourself from writing a bad Not type family?"
--
-- This is a great question and I stumbled at the time but it came
-- to me later. Just as we might write a test for our `not` function
-- to ensure it has the right property, for type-level functions we
-- instead write propositions, which are witnessed (or proven) by writing
-- functions to adhere to them.
--
-- In the case of `not`, we want to write the proposition that:
--
-- not a != a
--
-- that is, `not` is really, truly not the identity!
--
-- But, how do we do this in Haskell? It's a bit clumsy, and to be honest
-- I'm not really sure I understand it so well myself, but I think you do it
-- as follows:
-- 1. write a type family for Not
-- 2. write a type family to encode type equality
-- 3. show that (Not a == a) has the type "False"
-- 
-- we achieve #3 via our singleon GADT SBool and writing a function
-- with the signature:
--
-- notIsNotIdentity :: SBool a -> SBool (Not a == a)
--
-- whose value for any `a` results in SFalse.
--
-- I believe that in an actual languag with dependent types we'd represent
-- Not a == a by using bottom (⊥), but since we don't have that and I'm not
-- totally sure how to represent judgements in Haskell's type system (if
-- that's even the right term) this was the only way I could figure out how to
-- do it. (for example, in Agda you can translate judgements to their bool type,
-- as you can see here with the function `T`: 
-- http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Bool.agda)
--
-- to be honest I'm a bit out of my element. halp?
--
-- let me know your thouhgts! vilevin [at] gmail [dot] com

-- | our Bools
data Bool = True | False

-- | Singleton for Bools
data SBool (b :: Bool) where
    STrue  :: SBool True
    SFalse :: SBool False

-- | our Not type-level function
type family Not (b :: Bool) :: Bool where
    Not True  = False
    Not False = True

-- | a type level function to represent when two types are not equal
type family (a :: k) == (b :: k) :: Bool where
    a == a = True
    a == b = False

infix 4 ==

-- | our not
not :: SBool b -> SBool (Not b)
not STrue = SFalse
not SFalse = STrue

-- | One property of booleans is the following:
-- not a != a
-- we encode this proposition via curry-howard isomorphism by
-- writing a function that, when given any `SBool a`, it must
-- be the case that `Not a == a` is False, and therefore we
-- must return `SFalse` for each value of `SBool a`.
notIsNotIdentity :: SBool a -> SBool (Not a == a)
notIsNotIdentity STrue = SFalse
notIsNotIdentity SFalse = SFalse

@stebulus I guess technically you could just write two functions?