src/Symantic/Typer/List.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE PolyKinds #-}
   3
   4 module Symantic.Typer.List where
   5
   6 import Data.Function (($), (.))
   7 import Data.Int (Int)
   8 import Text.Show (Show (..))
   9 import Prelude qualified
  10
  11 -- * Type family @(++)@
  12 type family (++) xs ys where
  13   '[] ++ ys = ys
  14   -- xs  ++ '[] = xs
  15   (x ': xs) ++ ys = x ': xs ++ ys
  16 infixr 5 ++
  17
  18 -- * Type 'Len'
  19 data Len (xs :: [k]) where
  20   LenZ :: Len '[]
  21   LenS :: Len xs -> Len (x ': xs)
  22
  23 instance Show (Len vs) where
  24   showsPrec _p = showsPrec 10 . intLen
  25
  26 addLen :: Len a -> Len b -> Len (a ++ b)
  27 addLen LenZ b = b
  28 addLen (LenS a) b = LenS $ addLen a b
  29
  30 shiftLen :: forall t b a. Len a -> Len (a ++ b) -> Len (a ++ t ': b)
  31 shiftLen LenZ b = LenS b
  32 shiftLen (LenS a) (LenS b) = LenS $ shiftLen @t @b a b
  33
  34 intLen :: Len xs -> Int
  35 intLen = go 0
  36   where
  37     go :: Int -> Len xs -> Int
  38     go i LenZ = i
  39     go i (LenS l) = go (1 Prelude.+ i) l
  40
  41 -- ** Class 'LenInj'
  42 class LenInj (vs :: [k]) where
  43   lenInj :: Len vs
  44 instance LenInj '[] where
  45   lenInj = LenZ
  46 instance LenInj as => LenInj (a ': as) where
  47   lenInj = LenS lenInj