Singletons.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}

module Singletons where

import Data.Kind (Type)
-- import GHC.TypeNats

canMakeMove :: Int -> Int -> Either [Char] Bool
canMakeMove n m
  | n == m = Left "Can't call function w/ equal args!"
  | n > m  = Right True
  | n < m  = Right False

-- foo :: 5
-- foo = undefined

foo2 :: (a :: Type)
foo2 = undefined

-- Singleton:
--
--

data Nat     -- defines the "kind" Nat
  = Zero     -- defines the "type" Zero
  | Succ Nat -- defines the "type" Succ Nat

data SNat (n :: Nat) where
  SZero :: SNat 'Zero
  SSucc :: SNat n -> SNat ('Succ n)

type family (:==:) (a :: k) (b :: k) where
  x :==: x = 'True
  x :==: y = 'False

f :: SNat 'Zero
f = SZero

instance Eq (SNat 'Zero) where
  SZero /= SZero = False

instance Eq (SNat n) => Eq (SNat ('Succ n)) where
  SSucc n /= SZero = True
  SSucc n /= SSucc m = n /= m

sCanMakeMove :: ((n :==: m) ~ 'False) => SNat n -> SNat m -> Bool
sCanMakeMove n m = True