Окунув носок в воды зависимых типов, я обнаружил трещину в каноническом примере со списком статически типизированной длины.

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

-- a kind declaration
data Nat = Z | S Nat

data SafeList :: (Nat -> * -> *) where
    Nil :: SafeList Z a
    Cons :: a -> SafeList n a -> SafeList (S n) a

-- the type signature ensures that the input list has at least one element
safeHead :: SafeList (S n) a -> a
safeHead (Cons x xs) = x

Это похоже на работу:

ghci> :t Cons 5 (Cons 3 Nil)
Cons 5 (Cons 3 Nil) :: Num a => SafeList ('S ('S 'Z)) a

ghci> safeHead (Cons 'x' (Cons 'c' Nil))
'x'

ghci> safeHead Nil
Couldn't match type 'Z with 'S n0
Expected type: SafeList ('S n0) a0
  Actual type: SafeList 'Z a0
In the first argument of `safeHead', namely `Nil'
In the expression: safeHead Nil
In an equation for `it': it = safeHead Nil

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

fromList :: [a] -> SafeList n a
fromList = foldr Cons Nil

Это не скомпилируется, с ошибкой типа:

Couldn't match type 'Z with 'S n
Expected type: a -> SafeList n a -> SafeList n a
  Actual type: a -> SafeList n a -> SafeList ('S n) a
In the first argument of `foldr', namely `Cons'
In the expression: foldr Cons Nil
In an equation for `fromList': fromList = foldr Cons Nil

Я понимаю, почему это происходит: тип возвратаCons отличается для каждой итерации сгиба - вот и весь смысл! Но я не могу найти способ обойти это, вероятно, потому что я недостаточно глубоко вник в предмет. (Я не могу себе представить, что все эти усилия вкладываются в систему типов, которую невозможно использовать на практике!)

Итак: Как я могу построить этот тип зависимых данных из «обычных» данных простого типа?

Следуя совету @ Luqui, я смог сделатьfromList компиляции:

data ASafeList a where
    ASafeList :: SafeList n a -> ASafeList a

fromList :: [a] -> ASafeList a
fromList = foldr f (ASafeList Nil)
    where f x (ASafeList xs) = ASafeList (Cons x xs)

Вот моя попытка распаковатьASafeList и использовать это:

getSafeHead :: [a] -> a
getSafeHead xs = case fromList xs of ASafeList ys -> safeHead ys

Это вызывает другую ошибку типа:

Couldn't match type `n' with 'S n0
  `n' is a rigid type variable bound by
      a pattern with constructor
        ASafeList :: forall a (n :: Nat). SafeList n a -> ASafeList a,
      in a case alternative
      at SafeList.hs:33:22
Expected type: SafeList ('S n0) a
  Actual type: SafeList n a
In the first argument of `safeHead', namely `ys'
In the expression: safeHead ys
In a case alternative: ASafeList ys -> safeHead ys

Опять же, интуитивно понятно, что это не скомпилируется. я могу позвонитьfromList с пустым списком, поэтому у компилятора нет гарантии, что я смогу вызватьsafeHead в результатеSafeList, Этот недостаток знаний примерно то, что экзистенциальныйASafeList захватывает.

Можно ли решить эту проблему? Я чувствую, что, возможно, ушел в логический тупик.