
  0 | module Data.Singleton
  1 | 
  2 | import Decidable.Equality
  3 | 
  4 | %default total
  5 | 
  6 | ||| The type containing only a particular value.
  7 | ||| This is useful for calculating type-level information at runtime.
  8 | public export
  9 | data Singleton : a -> Type where
 10 |      Val : (x : a) -> Singleton x
 11 | 
 12 | public export %inline
 13 | reindex : (0 _ : x === y) -> Singleton x -> Singleton y
 14 | reindex Refl x = x
 15 | 
 16 | public export %inline
 17 | unVal : Singleton {a} x -> a
 18 | unVal $ Val x = x
 19 | 
 20 | public export %inline
 21 | (.unVal) : Singleton {a} x -> a
 22 | (.unVal) = unVal
 23 | 
 24 | -- pure and <*> implementations for idiom bracket notation
 25 | 
 26 | public export
 27 | pure : (x : a) -> Singleton x
 28 | pure = Val
 29 | 
 30 | public export
 31 | (<*>) : Singleton f -> Singleton x -> Singleton (f x)
 32 | Val f <*> Val x = Val (f x)
 33 | 
 34 | public export %inline
 35 | Eq (Singleton v) where
 36 |   _ == _ = True
 37 | 
 38 | public export %inline
 39 | Ord (Singleton v) where
 40 |   compare _ _ = EQ
 41 | 
 42 | public export %inline
 43 | Semigroup (Singleton v) where
 44 |   x <+> _ = x
 45 | 
 46 | public export %inline
 47 | {v : a} -> Monoid (Singleton v) where
 48 |   neutral = Val v
 49 | 
 50 | export
 51 | Show a => Show (Singleton {a} v) where
 52 |   showPrec p (Val v) = showCon p "Val" (showArg v)
 53 | 
 54 | export
 55 | DecEq (Singleton v) where
 56 |   decEq (Val v) (Val v) = Yes Refl
 57 |