Можно ли составить размерный список, используя одноэлементные Натс (например, 0, 1, ...) из списков в Haskell?

Question

Изучая синглтоны и (полу) зависимую типизацию, я начал пытаться составить список размеров из обычного списка на Haskell с размерами, заданными Натсом, такими как 0, 1, 2, 3, ... вместо Z, SZ , S (SZ) и т. Д. Я использую библиотеку Data.Singletons.TypeLits, кстати. (одиночки-2.5.1).

Вот как я пытался это сделать:

data NatList (a :: *) (n :: Nat) where
    Nah :: NatList a 0
    Yea :: a -> NatList a n -> NatList a (n + 1)

fromList :: SNat n -> [a] -> NatList a n
fromList s []     = Nah
fromList s (x:xs) = Yea x (fromList (s %- (SNat :: SNat 1)) xs)

Этот код не компилируется и выдает ошибку

"Невозможно сопоставить тип" n "с" 0 " ‘N’ - это переменная жесткого типа, связанная подпись типа для: fromList :: forall (n :: Nat) a. SNat n -> [a] -> NatList a n

Answer 1

Ваша подпись для fromList говорит, что она работает для любого типа n :: Nat. Но первое уравнение возвращает Nah, что требует n для типа 0.

Так что fromList должен быть методом класса, который может отправлять по типу n.

Но вы пытаетесь отправить значение второго аргумента fromList - то есть, в списке пустом или нет - в зависимый тип. Библиотека / техника Singletons предназначена для фальсификации зависимых типов в Haskell. И вот где мои знания заканчиваются. Поэтому я использую Peano Nats S Z с экземплярами, а не с GADT.

Answer 2

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

data SizedList (a :: *) (n :: Nat) where
    Nil  :: SizedList a 0
    Cons :: a -> SizedList a n -> SizedList a (n+1)

data SomeSL (a :: *) where
    MkSomeSL :: KnownNat n => SNat n -> SizedList a n -> SomeSL a  

toList :: SizedList a n -> [a]
toList Nil         = []
toList (Cons x xs) = x : toList xs

fromList :: [a] -> SomeSL a
fromList []     = MkSomeSL (SNat @0) Nil 
fromList (x:xs) = case (fromList xs) of 
    MkSomeSL n ys -> MkSomeSL (n %+ SNat @1) (Cons x ys)

toList_ :: SomeSL a -> [a]
toList_ (MkSomeSL _ xs) = toList xs

Здесь SomeSL переносит тип SizedList из моего вопроса вместе с одноэлементным nat, позволяя функциям получать доступ к длине через SNat n.

Серия постов Джастина Ле о блогах была очень полезна: https://blog.jle.im/entry/introduction-to-singletons-1.html

Answer 3

Я не знаю эту библиотеку, но, насколько я понимаю, проблема заключается в первом предложении fromList, которое должно совпадать только при n = 0.

--...
fromList 0 []     = Nah
--...