Индекс гетерогенного списка

Question

Я построил гетерогенный Список в Haskell, используя некоторое программирование на уровне типов.

data HList a where
  Singleton :: HList '[]
  Cons :: h -> HList t -> HList (h ': t)

Теперь я хотел бы иметь возможность индексировать этот список, однако есть некоторые проблемы с типами, которые делают это очень труднымдля меня.Я могу очень легко получить начало или конец этого списка

head :: HList (h ': t) -> h
head (Cons a _) = a

tail :: HList (h ': t) -> HList t
tail (Cons _ b) = b

Однако индексирование списка очень отличается, потому что тип вывода зависит от того, какой индекс мы передаем.Так что наивно наш тип будет выглядеть примерно так:

fromIndex :: (Num a) => a -> (HList b) -> ???

Однако определить ??? довольно сложно.Так что вместо Num нам придется взять что-то еще.Моя идея (код ниже) состояла в том, чтобы создать новый класс Natural и IndexType с функциональной зависимостью, который позволил бы нам найти тип результата только из типов ввода.

{-# Language GADTs, DataKinds, TypeOperators, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}

data Nat = Z | S Nat

data Natural a where
  Zero :: Natural 'Z
  Succ :: Natural a -> Natural ('S a)

data HList a where
 Singleton :: HList '[]
 Cons :: h -> HList t -> HList (h ': t)

class IndexType a b c | a b -> c
instance IndexType (Natural 'Z) (HList (h ': t)) h
instance IndexType (Natural n) (HList t) a => IndexType (Natural ('S n)) (HList (h ': t)) a

fromIndex :: (IndexType (Natural n) (HList l) a) => (Natural n) -> (HList l) -> a
fromIndex (Zero) (Cons x Singleton) = x
fromIndex (Succ a) (Cons _ (xs)) = fromIndex a xs

Наш IndexType класс работает.Если я тестирую только класс типов

class Test a | -> a
  where test :: a
instance (IndexType (Natural ('S ('S ('S 'Z)))) (HList (Int ': String ': Char ': (Int -> String) ': Int ': '[])) a) => Test a

, мы получаем правильный результат:

*Main> :t test
test :: Int -> String

Однако ghc не может проверить сигнатуру нашего типа, и мы получаем довольно монолитную ошибку:

test.hs:28:39: error:
    • Could not deduce: h ~ a
      from the context: n ~ 'Z
        bound by a pattern with constructor: Zero :: Natural 'Z,
                 in an equation for ‘fromIndex’
        at test.hs:28:12-15
      or from: l ~ (h : t)
        bound by a pattern with constructor:
                   Cons :: forall h (t :: [*]). h -> HList t -> HList (h : t),
                 in an equation for ‘fromIndex’
        at test.hs:28:19-34
      or from: t ~ '[]
        bound by a pattern with constructor: Singleton :: HList '[],
                 in an equation for ‘fromIndex’
        at test.hs:28:26-34
      ‘h’ is a rigid type variable bound by
        a pattern with constructor:
          Cons :: forall h (t :: [*]). h -> HList t -> HList (h : t),
        in an equation for ‘fromIndex’
        at test.hs:28:19-34
      ‘a’ is a rigid type variable bound by
        the type signature for:
          fromIndex :: forall (n :: Nat) (l :: [*]) a.
                       IndexType (Natural n) (HList l) a =>
                       Natural n -> HList l -> a
        at test.hs:27:1-81
    • In the expression: x
      In an equation for ‘fromIndex’:
          fromIndex (Zero) (Cons x Singleton) = x
    • Relevant bindings include
        x :: h (bound at test.hs:28:24)
        fromIndex :: Natural n -> HList l -> a (bound at test.hs:28:1)
   |
28 | fromIndex (Zero) (Cons x Singleton) = x
   |                                       ^

test.hs:29:36: error:
    • Could not deduce (IndexType (Natural a1) (HList t) a)
        arising from a use of ‘fromIndex’
      from the context: IndexType (Natural n) (HList l) a
        bound by the type signature for:
                   fromIndex :: forall (n :: Nat) (l :: [*]) a.
                                IndexType (Natural n) (HList l) a =>
                                Natural n -> HList l -> a
        at test.hs:27:1-81
      or from: n ~ 'S a1
        bound by a pattern with constructor:
                   Succ :: forall (a :: Nat). Natural a -> Natural ('S a),
                 in an equation for ‘fromIndex’
        at test.hs:29:12-17
      or from: l ~ (h : t)
        bound by a pattern with constructor:
                   Cons :: forall h (t :: [*]). h -> HList t -> HList (h : t),
                 in an equation for ‘fromIndex’
        at test.hs:29:21-31
    • In the expression: fromIndex a xs
      In an equation for ‘fromIndex’:
          fromIndex (Succ a) (Cons _ (xs)) = fromIndex a xs
   |
29 | fromIndex (Succ a) (Cons _ (xs)) = fromIndex a xs
   |                                    ^^^^^^^^^^^^^^
Failed, no modules loaded.

Можно ли построить функцию индексации?Есть ли способ заставить GHC сделать вывод, что моя подпись типа верна?

Answer 1

Я бы определил следующее:

-- The type of numbers n such that xs !! n = x
-- Compare to Nat
data Elem (x :: k) (xs :: [k]) where
  Here  :: Elem x (x : xs)
  There :: Elem x xs -> Elem x (y : xs)

И тогда вы обнаружите, что HList s изоморфны "функциям индексации" (таким же образом Vect n a изоморфно Fin n -> a)включая этот тип:

indexHList :: forall xs. HList xs -> (forall x. Elem x xs -> x)
indexHList (Cons x _) Here = x
indexHList (Cons _ xs) (There i) = indexHList xs i
indexHList Singleton impossible = case impossible of {}

-- unindexHList ::ish forall xs. (forall x. Elem x xs -> x) -> HList xs
-- is a bit more work (and doesn't really have that type)
-- but is conceptually the other half of the isomorphism.

Использование:

xs :: HList [Int, String, HList '[]]
xs = Cons 5 $ Cons "hello" $ Cons Singleton $ Singleton
-- Here :: Elem Int (Int:_)
indexHList xs Here == 5
-- Here :: Elem String (String:_)
-- There Here :: Elem String (_:String:_)
indexHList xs (There Here) == "hello"

По сравнению с вашей class техникой, Elem x xs в основном exists n. (Natural n, IndexType (Natural n) (HList xs) x).Будучи типом данных, который вы можете проверить, им легче манипулировать, чем классом.

Answer 2

Случаи вашего fromIndex бывают разных типов!Они должны быть внутри экземпляров

class IndexType (n :: Nat) (xs :: [Type]) (i :: Type) | n xs -> i where
   fromIndex :: Natural n -> HList xs -> i

 instance IndexType Z (x ': xs) x where
   fromIndex Zero (Cons x _) = x

 instance IndexType n xs a => IndexType (S n) (x ': xs) a where
   fromIndex (Succ n) (Cons _ xs) = fromIndex n xs

(я немного перемешал тип fromIndex :: Natural n -> HList xs -> i. На самом деле это ничего не меняет - ваше решение работает так же хорошо, хотя и с более запутанной ошибкойсообщения, если вы звоните fromIndex в неожиданном контексте.)