blob: e9460371c86357bd5ae32d02e4e87924b3ec4f30 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
{-# OPTIONS_GHC -Wincomplete-patterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE EmptyCase #-}
module Fin (Nat (..), Fin (FZ, FS)) where
import Numeric.Natural
import Unsafe.Coerce
data Nat = Z | S Nat
-- Fin *must* be exported abstractly (or placed in an Unsafe
-- module) to maintain type safety.
newtype Fin (n :: Nat) = Fin Natural
data FinView n where
VZ :: FinView ('S n)
VS :: !(Fin n) -> FinView ('S n)
viewFin :: Fin n -> FinView n
viewFin (Fin 0) = unsafeCoerce VZ
viewFin (Fin n) = unsafeCoerce (VS (Fin (n - 1)))
pattern FZ :: () => n ~ 'S m => Fin n
pattern FZ <- (viewFin -> VZ) where
FZ = Fin 0
pattern FS :: () => n ~ 'S m => Fin m -> Fin n
pattern FS m <- (viewFin -> VS m) where
FS (Fin m) = Fin (1 + m)
{-# COMPLETE FZ, FS #-}
finZAbsurd :: Fin 'Z -> a
finZAbsurd x = case x of
|
