В образовательных целях я пытался реконструировать пример из книги "тип-управляемое развитие с Идрисом" (а именно 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 v@ is the proposition that an element of type @a@
-- is contained in a vector of type @v@. To be useful, @a@ and @v@
-- 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 не используется явно с другим доказательством.