• code Haskell
    вот вопрос похоже исчерпан
    ```
    {-# LANGUAGE TypeInType, GADTs, TypeFamilies, UndecidableInstances #-}
    import Data.Kind (Type)
    
    data N = Z | S N
    
    data Fin :: N -> Type where
      FZ :: Fin (S n)
      FS :: Fin n -> Fin (S n)
    
    type family FieldCount (t :: Type) :: N
    
    type family FieldTypeI (t :: Type) (i :: N) :: Type
    type family FieldType (t :: Type) (i :: Fin p) where
      FieldType t i = FieldTypeI t (F2II (AsQ t i))
    
    type family AsQ (t :: Type) (i :: Fin n) :: Fin (FieldCount t) where
      AsQ t i = Cast (FieldCount t) i
    
    type family Cast (t :: N) (i :: Fin n) :: Fin t where
      Cast (S Z) FZ = FZ
      Cast (S n) FZ = FZ
      Cast (S n) (FS k) = FS (Cast n k)
    
    
    type family F2II (a :: Fin n) :: N where
      F2II (FS n) = S (F2II n)
      F2II FZ = Z
    
    data T
    
    type instance FieldCount T = S (S (S Z))
    type instance FieldTypeI T Z = Int
    type instance FieldTypeI T (S Z) = Bool
    ```

Replies (2)