symantic/Language/Symantic/Typing/List.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE PolyKinds #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5 -- | List utilities at the type-level.
   6 module Language.Symantic.Typing.List where
   7
   8 import GHC.Exts (Constraint)
   9
  10 import Language.Symantic.Typing.Peano
  11
  12 -- ** Type 'Index'
  13 -- | Return the position of a type within a list of them.
  14 -- This is useful to work around @OverlappingInstances@.
  15 type family Index xs x where
  16         Index (x     ': xs) x = Zero
  17         Index (not_x ': xs) x = Succ (Index xs x)
  18
  19 -- * Type family @(++)@
  20 type family (++) xs ys where
  21         '[] ++ ys  = ys
  22         -- xs  ++ '[] = xs
  23         (x ': xs) ++ ys = x ': xs ++ ys
  24 infixr 5 ++
  25
  26 -- * Type family 'Concat'
  27 type family Concat (xs::[[k]]) :: [k] where
  28         Concat '[] = '[]
  29         Concat (x ': xs) = x ++ Concat xs
  30
  31 -- * Type family 'Concat_Constraints'
  32 type family Concat_Constraints (cs::[Constraint]) :: Constraint where
  33         Concat_Constraints '[] = ()
  34         Concat_Constraints (c ': cs) = (c, Concat_Constraints cs)
  35
  36 -- * Type family 'DeleteAll'
  37 type family DeleteAll (x::k) (xs::[k]) :: [k] where
  38         DeleteAll x '[] = '[]
  39         DeleteAll x (x ': xs) = DeleteAll x xs
  40         DeleteAll x (y ': xs) = y ': DeleteAll x xs
  41
  42 -- * Type family 'Head'
  43 type family Head (xs::[k]) :: k where
  44         Head (x ': _xs) = x
  45
  46 -- * Type family 'Tail'
  47 type family Tail (xs::[k]) :: [k] where
  48         Tail (_x ': xs) = xs
  49
  50 {-
  51 -- * Type family 'Map'
  52 type family Map (f::a -> b) (cs::[a]) :: [b] where
  53         Map f '[] = '[]
  54         Map f (c ': cs) = f c ': Map f cs
  55 -}
  56
  57 -- * Type family 'Nub'
  58 type family Nub (xs::[k]) :: [k] where
  59         Nub '[] = '[]
  60         Nub (x ': xs) = x ': Nub (DeleteAll x xs)
  61
  62 {-
  63 -- * Type family 'L'
  64 type family L (xs::[k]) :: Nat where
  65         L '[] = 'Z
  66         L (x ': xs) = 'S (L xs)
  67
  68 -- ** Class 'LInj'
  69 class LInj (as::[k]) where
  70         lInj :: SNat (L as)
  71 instance LInj '[] where
  72         lInj = SNatZ
  73 instance LInj as => LInj (a ': as) where
  74         lInj = SNatS (lInj @_ @as)
  75 -}
  76
  77 -- * Type 'Len'
  78 data Len (xs::[k]) where
  79         LenZ :: Len '[]
  80         LenS :: Len xs -> Len (x ': xs)
  81
  82 instance Show (Len vs) where
  83         showsPrec _p = showsPrec 10 . intLen
  84
  85 addLen :: Len a -> Len b -> Len (a ++ b)
  86 addLen LenZ     b = b
  87 addLen (LenS a) b = LenS $ addLen a b
  88
  89 shiftLen ::
  90  forall t b a.
  91  Len a ->
  92  Len (a ++      b) ->
  93  Len (a ++ t ': b)
  94 shiftLen LenZ b = LenS b
  95 shiftLen (LenS a) (LenS b) = LenS $ shiftLen @t @b a b
  96
  97 intLen :: Len xs -> Int
  98 intLen = go 0
  99         where
 100         go :: Int -> Len xs -> Int
 101         go i LenZ     = i
 102         go i (LenS l) = go (1 + i) l
 103
 104 -- ** Class 'LenInj'
 105 class LenInj (vs::[k]) where
 106         lenInj :: Len vs
 107 instance LenInj '[] where
 108         lenInj = LenZ
 109 instance LenInj as => LenInj (a ': as) where
 110         lenInj = LenS lenInj