{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
-----------------------------------------------------------------------------
-- |
-- Module : Data.Type.Fin
-- Copyright : Copyright (C) 2015 Kyle Carter
-- License : BSD3
--
-- Maintainer : Kyle Carter <kylcarte@indiana.edu>
-- Stability : experimental
-- Portability : RankNTypes
--
-- A @singleton@-esque type for representing members of finite sets.
--
-----------------------------------------------------------------------------
module Data.Type.Fin where
import Data.Type.Nat
import Type.Class.Higher
import Type.Class.Known
import Type.Class.Witness
import Type.Family.Constraint
import Type.Family.Nat
-- import Data.Type.Quantifier
data Fin :: N -> * where
FZ :: Fin (S n)
FS :: !(Fin n) -> Fin (S n)
deriving instance Eq (Fin n)
deriving instance Ord (Fin n)
deriving instance Show (Fin n)
instance Eq1 Fin
instance Ord1 Fin
instance Show1 Fin
instance Read1 Fin where
readsPrec1 d = readParen (d > 10) $ \s0 ->
[ (Some FZ,s1)
| ("FZ",s1) <- lex s0
] ++
[ (n >>- Some . FS,s2)
| ("FS",s1) <- lex s0
, (n,s2) <- readsPrec1 11 s1
]
instance (Known Nat n, Pos n) => Enum (Fin n) where
toEnum n
| n <= 0 = FZ
| otherwise = case (known :: Nat n) of
S_ Z_ -> FZ
S_ S_{} -> FS $ toEnum (n-1)
fromEnum = fin
instance (Known Nat n, Pos n) => Bounded (Fin n) where
minBound = FZ
maxBound = case (known :: Nat n) of
S_ Z_ -> FZ
S_ S_{} -> FS maxBound
elimFin :: (forall x. p (S x))
-> (forall x. Fin x -> p x -> p (S x))
-> Fin n -> p n
elimFin z s = \case
FZ -> z
FS n -> s n $ elimFin z s n
-- | Gives the list of all members of the finite set of size @n@.
fins :: Nat n -> [Fin n]
fins = \case
Z_ -> []
S_ x -> FZ : map FS (fins x)
fin :: Fin n -> Int
fin = \case
FZ -> 0
FS x -> succ $ fin x
-- | There are no members of @Fin Z@.
finZ :: Fin Z -> Void
finZ = impossible
weaken :: Fin n -> Fin (S n)
weaken = \case
FZ -> FZ
FS n -> FS $ weaken n
-- | Map a finite set to a lower finite set without
-- one of its members.
without :: Fin n -> Fin n -> Maybe (Fin (Pred n))
without = \case
FZ -> \case
FZ -> Nothing
FS y -> Just y
FS x -> \case
FZ -> Just FZ \\ x
FS y -> FS <$> without x y \\ x
-- | Take a 'Fin' to an existentially quantified 'Nat'.
finNat :: Fin x -> Some Nat
finNat = \case
FZ -> Some Z_
FS x -> withSome (Some . S_) $ finNat x
-- | A @Fin n@ is a 'Witness' that @n >= 1@.
--
-- That is, @'Pred' n@ is well defined.
instance (n' ~ Pred n) => Witness ØC (S n' ~ n) (Fin n) where
type WitnessC ØC (S n' ~ n) (Fin n) = (n' ~ Pred n)
(\\) r = \case
FZ -> r
FS _ -> r