Доказательство неравенства типа для GHC


В образовательных целях я пытался реконструировать пример из книги "тип-управляемое развитие с Идрисом" (а именно RemoveElem.idr ) в Haskell посредством использования различных языковых расширений и синглетных типов. Суть его заключается в функции, которая удаляет элемент из непустого вектора, получив доказательство того, что элемент действительно находится в векторе. Следующий код является автономным (GHC 8.4 или более поздней версии). Проблема возникает в самом начале. конец:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind
import Data.Type.Equality
import Data.Void

-- | Inductively defined natural numbers.
data Nat = Z | S Nat deriving (Eq, Show)

-- | Singleton types for natural numbers.
data SNat :: Nat -> Type where
    SZ :: SNat 'Z
    SS :: SNat n -> SNat ('S n)

deriving instance Show (SNat n)

-- | "Demote" a singleton-typed natural number to an ordinary 'Nat'.
fromSNat :: SNat n -> Nat
fromSNat SZ = Z
fromSNat (SS n) = S (fromSNat n)

-- | A decidable proposition.
data Dec a = Yes a | No (a -> Void)

-- | Propositional equality of natural numbers.
eqSNat :: SNat a -> SNat b -> Dec (a :~: b)
eqSNat  SZ     SZ    = Yes Refl
eqSNat  SZ    (SS _) = No (case {})
eqSNat (SS _)  SZ    = No (case {})
eqSNat (SS a) (SS b) = case eqSNat a b of
    No  f    -> No (case Refl -> f Refl)
    Yes Refl -> Yes Refl

-- | A length-indexed list (aka vector).
data Vect :: Nat -> Type -> Type where
    Nil   :: Vect 'Z a
    (:::) :: a -> Vect n a -> Vect ('S n) a

infixr 5 :::

deriving instance Show a => Show (Vect n a)

-- | @Elem a [email protected] is the proposition that an element of type @[email protected]
-- is contained in a vector of type @[email protected] To be useful, @[email protected] and @[email protected]
-- need to refer to singleton types.
data Elem :: forall a n. a -> Vect n a -> Type where
    Here  :: Elem x (x '::: xs)
    There :: Elem x xs -> Elem x (y '::: xs)

deriving instance Show a => Show (Elem a v)

------------------------------------------------------------------------
-- From here on, to simplify things, only vectors of natural
-- numbers are considered.

-- | Singleton types for vectors of 'Nat's.
data SNatVect :: forall n. Nat -> Vect n Nat -> Type where
    SNatNil  :: SNatVect 'Z 'Nil
    SNatCons :: SNat a -> SNatVect n v -> SNatVect ('S n) (a '::: v)

deriving instance Show (SNatVect n v)

-- | "Demote" a singleton-typed vector of 'SNat's to an
-- ordinary vector of 'Nat's.
fromSNatVect :: SNatVect n v -> Vect n Nat
fromSNatVect SNatNil = Nil
fromSNatVect (SNatCons a v) = fromSNat a ::: fromSNatVect v

-- | Decide whether a value is in a vector.
isElem :: SNat a -> SNatVect n v -> Dec (Elem a v)
isElem _  SNatNil        = No (case {})
isElem a (SNatCons b as) = case eqSNat a b of
    Yes Refl   -> Yes Here
    No notHere -> case isElem a as of
        Yes there   -> Yes (There there)
        No notThere -> No $ case
            Here        -> notHere Refl
            There there -> notThere there

type family RemoveElem (a :: Nat) (v :: Vect ('S n) Nat) :: Vect n Nat where
    RemoveElem a (a '::: as) = as
    RemoveElem a (b '::: as) = b '::: RemoveElem a as

-- | Remove a (singleton-typed) element from a (non-empty, singleton-typed)
-- vector, given a proof that the element is in the vector.
removeElem :: forall (a :: Nat) (v :: Vect ('S n) Nat)
    . SNat a
    -> Elem a v
    -> SNatVect ('S n) v
    -> SNatVect n (RemoveElem a v)
removeElem x prf (SNatCons y ys) = case prf of
    Here        -> ys
    There later -> case ys of
        SNatNil    -> case later of {}
        SNatCons{} -> SNatCons y (removeElem x later ys)
            -- ^ Could not deduce:
            --            RemoveElem a (y '::: (a2 '::: v2))
            --          ~ (y '::: RemoveElem a (a2 '::: v2))
Очевидно, система типов нуждается в убеждении, что типы значений x и y не могут быть равны в этой ветви кода, так что второе уравнение семейства типов может быть однозначно использовано для уменьшения возвращаемого типа по мере необходимости. Я не знаю, как это сделать. Наивно, я хотел бы, чтобы конструктор There и, таким образом, совпадение шаблона на There later несли / показывали доказательство неравенства типа в GHC.

Следующее является явно избыточным и частичное решение, которое просто демонстрирует неравенство типов, необходимое для проверки типа GHC рекурсивным вызовом:

        SNatCons{} -> case (x, y) of
            (SZ, SS _) -> SNatCons y (removeElem x later ys)
            (SS _, SZ) -> SNatCons y (removeElem x later ys)

Теперь, например, это работает:

λ> let vec = SNatCons SZ (SNatCons (SS SZ) (SNatCons SZ SNatNil))
λ> :t vec
vec
  :: SNatVect ('S ('S ('S 'Z))) ('Z '::: ('S 'Z '::: ('Z '::: 'Nil)))
λ> let Yes prf = isElem (SS SZ) vec
λ> :t prf
prf :: Elem ('S 'Z) ('Z '::: ('S 'Z '::: ('Z '::: 'Nil)))
λ> let vec' = removeElem (SS SZ) prf vec
λ> :t vec'
vec' :: SNatVect ('S ('S 'Z)) ('Z '::: ('Z '::: 'Nil))
λ> fromSNatVect vec'
Z ::: (Z ::: Nil)

Разрешение

Как намекнуто в комментарии @chi и подробно описано в ответе HTNW, я пытался решить неправильную проблему, написав removeElem с вышеуказанной сигнатурой типа и семейством типов, и если бы я смог, то полученная программа была бы плохо типизирована.

В ниже приведены исправления, которые я сделал на основе ответа HTNW (возможно, вы захотите прочитать его, прежде чем продолжить здесь).

Первой ошибкой или ненужным усложнением было повторение длины вектора в типе SNatVects. Я думал, что это необходимо для того, чтобы написать fromSNatVect, но это, конечно, не так:
data SNatVect (v :: Vect n Nat) :: Type where
    SNatNil  :: SNatVect 'Nil
    SNatCons :: SNat a -> SNatVect v -> SNatVect (a '::: v)

deriving instance Show (SNatVect v)

fromSNatVect :: forall (v :: Vect n Nat). SNatVect v -> Vect n Nat
-- implementation unchanged
Теперь есть два подхода к написанию

. Первый берет Elem, an SNatVect и возвращает a Vect:

removeElem :: forall (a :: Nat) (n :: Nat) (v :: Vect ('S n) Nat)
    . Elem a v
    -> SNatVect v
    -> Vect n Nat
removeElem prf (SNatCons y ys) = case prf of
    Here        -> fromSNatVect ys
    There later -> case ys of
        SNatNil    -> case later of {}
        SNatCons{} -> fromSNat y ::: removeElem later ys

Второй берет SElem, an SNatVect и возвращает SNatVect, используя семейство типов RemoveElem, которое отражает функцию уровня значения:

data SElem (e :: Elem a (v :: Vect n k)) where
    SHere  :: forall x xs. SElem ('Here :: Elem x (x '::: xs))
    SThere :: forall x y xs (e :: Elem x xs). SElem e -> SElem ('There e :: Elem x (y '::: xs))

type family RemoveElem (xs :: Vect ('S n) a) (e :: Elem x xs) :: Vect n a where
    RemoveElem (x '::: xs) 'Here = xs
    RemoveElem (x '::: xs) ('There later) = x '::: RemoveElem xs later

sRemoveElem :: forall (xs :: Vect ('S n) Nat) (e :: Elem x xs)
    . SElem e
    -> SNatVect xs
    -> SNatVect (RemoveElem xs e)
sRemoveElem prf (SNatCons y ys) = case prf of
    SHere        -> ys
    SThere later -> case ys of
        SNatNil    -> case later of {}
        SNatCons{} -> SNatCons y (sRemoveElem later ys)

Интересно, что обе версии отказываются от передачи элемента для удаления в качестве отдельного аргумента, поскольку эта информация содержится в Elem / SElem ценность. Аргумент value также может быть удален из версии Idris этой функции, хотя тогда вариант removeElem_auto может быть немного запутанным, поскольку он будет иметь только вектор в качестве явного аргумента и удалит первый элемент вектора, если неявный аргумент prf не используется явно с другим доказательством.

1 8

1 ответ:

Рассмотрим [1, 2, 1]. RemoveElem 1 [1, 2, 1] есть [2, 1]. Теперь вызов removeElem 1 (There $ There $ Here) ([1, 2, 1] :: SNatVect 3 [1, 2, 1]) :: SNatVect 2 [2, 1] должен компилироваться. Это неправильно. Аргумент Elem говорит, чтобы удалить третий элемент, который дал бы [1, 2], но подпись типа говорит, что это должно быть [2, 1].

Во-первых, SNatVect Немного сломан. Он имеет два аргумента Nat:

data SNatVect :: forall n. Nat -> Vect n a -> Type where ...
Первый - это n, а второй-безымянный Nat. По структуре SNatVect они всегда равны. Это позволяет SNatVect удвоить доказательство равенства, но это, вероятно, не так намерение иметь его таким образом. Ты наверное имел ввиду
data SNatVect (n :: Nat) :: Vect n Nat -> Type where ...

Нет способа записать эту подпись в исходном Хаскелле, используя только обычный синтаксис ->. Однако, когда GHC печатает этот тип, вы иногда получаете

SNatVect :: forall (n :: Nat) -> Vect n Nat -> Type
Но это излишне. Вы можете взять Nat как неявный аргумент forall и вывести его из типа Vects:
data SNatVect (xs :: Vect n Nat) where
  SNatNil  :: SNatVect 'Nil
  SNatCons :: SNat x -> SNatVect xs -> SNatVect (x '::: xs)

Это дает

SNatVect :: forall (n :: Nat). Vect n Nat -> Type

Во-вторых, попробуйте написать

removeElem :: forall (n :: Nat) (x :: Nat) (xs :: Vect (S n) Nat).
              Elem x xs -> SNatVect xs -> Vect n Nat

Обратите внимание, как исчез аргумент SNat, и как тип возвращаемого значения является простым Vect. Аргумент SNat сделал тип "слишком большим", поэтому вы были пойманы на том, что он работает, когда функция просто не имеет смысла. Возвращаемый тип SNatVect означает, что вы пропускаете шаги. Грубо говоря, каждая функция имеет три формы: основную, f :: a -> b -> c; типовую, type family F (x :: a) (y :: b) :: c; и зависимую, f :: forall (x :: a) (y :: b). Sing x -> Sing y -> Sing (F x y). Каждый из них реализуется "одинаковым" способом, но попытка реализовать один без реализации его предшественников-это верный способ получить смущенный.

Теперь вы можете немного приподнять это:

data SElem (e :: Elem x (xs :: Vect n k)) where
  SHere :: forall x xs. SElem ('Here :: Elem x (x '::: xs))
  SThere :: forall x y xs (e :: Elem x xs). SElem e -> SElem ('There e :: Elem x (y '::: xs))

type family RemoveElem (xs :: Vect (S n) a) (e :: Elem x xs) :: Vect n a
Обратите внимание на взаимосвязь между типами removeElem и RemoveElem. Переупорядочивание аргументов происходит потому, что тип e зависит от xs, поэтому они должны быть упорядочены соответственно. Альтернативно: аргумент xs был переведен из forall ' d-и-неявно-задан в явно-заданный, а затем аргумент Sing xs был отменен, поскольку он не содержал никакой информации, поскольку был одиночка.

Наконец, вы можете написать эту функцию:

sRemoveElem :: forall (xs :: Vect (S n) Nat) (e :: Elem x xs).
               SElem e -> SNatVect xs -> SNatVect (RemoveElem xs e)