ch tauchte meinen Zeh in die Gewässer abhängiger Typen und hatte einen Riss in der kanonischen "Liste mit statisch typisierter Länge"

{-# 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

Dies scheint zu funktionieren:

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

Damit dieser Datentyp jedoch wirklich nützlich ist, sollte er aus Laufzeitdaten erstellt werden können, deren Länge Sie zur Kompilierungszeit nicht kennen. Mein naiver Versuch:

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

Dies kann nicht kompiliert werden, mit dem Typ Fehler:

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

Ich verstehe, warum das passiert: der Rückgabetyp vonCons ist für jede Iteration der Falte anders - das ist der springende Punkt! Aber ich sehe keinen Weg, wahrscheinlich, weil ich nicht tief genug in das Thema hineingelesen habe. (Ich kann mir nicht vorstellen, dass all dieser Aufwand in ein Typensystem gesteckt wird, das in der Praxis nicht anwendbar ist!)

So: Wie kann ich diese Art von abhängig typisierten Daten aus 'normalen' einfach typisierten Daten erstellen?

Folgen @ luquis Rat, den ich machen konntefromList compile:

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)

Hier ist mein Versuch, das @ auszupackASafeList und benutze es:

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

Dies verursacht einen anderen Typfehler:

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

Again, intuitiv macht es Sinn, dass dies nicht zu kompilieren wäre. Ich kann anrufenfromList mit einer leeren Liste, daher kann der Compiler nicht garantieren, dass ich @ anrufen kansafeHead auf dem resultierendenSafeList. Dieser Mangel an Wissen ist ungefähr das, was das existenzielleASafeList erfasst.

Kann dieses Problem gelöst werden? Ich habe das Gefühl, ich wäre in eine logische Sackgasse geraten.