Как создать список с зависимой длиной?

Ответ 1

Никогда ничего не бросайте.

Если вы столкнулись с трудностями, чтобы прокрутить список, чтобы сделать список с индексом длины (известный в литературе как "вектор" ), вы также можете запомнить его длину.

Итак, имеем

data Nat = Z | S Nat

data Vec :: Nat -> * -> * where -- old habits die hard
  VNil :: Vec Z a
  VCons :: a -> Vec n a -> Vec (S n) a

но мы также можем предоставить представление времени выполнения для статических длин. Пакет "Синглтоны" Ричарда Эйзенберга сделает это за вас, но основная идея - дать тип представлений времени выполнения для статических чисел.

data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

К сожалению, если у нас есть значение типа Natty n, тогда мы можем допросить это значение, чтобы узнать, что такое n.

Хашочисты знают, что представление времени исполнения часто настолько скучно, что даже машина может управлять им, поэтому мы скрываем его внутри класса типа

class NATTY (n :: Nat) where
  natty :: Natty n

instance NATTY Z where
  natty = Zy

instance NATTY n => NATTY (S n) where
  natty = Sy natty

Теперь мы можем дать немного более информативное экзистенциальное отношение к длине, которую вы получите из своих списков.

data LenList :: * -> * where
  LenList :: NATTY n => Vec n a -> LenList a

lenList :: [a] -> LenList a
lenList []        = LenList VNil
lenList (x : xs)  = case lenList xs of LenList ys -> LenList (VCons x ys)

Вы получаете тот же код, что и версия, разрушающая длину, но вы можете получить представление времени выполнения в любое время, которое вам нравится, и вам не нужно сканировать вдоль вектора, чтобы получить его.

Конечно, если вы хотите, чтобы длина была Nat, все равно боль, которая у вас вместо Natty n для n.

Ошибочно помешать одному карману.

Изменить. Я думал, что добавлю немного, чтобы решить проблему использования "безопасной главы".

Во-первых, позвольте мне добавить распаковщик для LenList, который дает вам номер в вашей руке.

unLenList :: LenList a -> (forall n. Natty n -> Vec n a -> t) -> t
unLenList (LenList xs) k = k natty xs

И теперь предположим, что я определяю

vhead :: Vec (S n) a -> a
vhead (VCons a _) = a

обеспечение безопасности. Если у меня есть представление длины вектора времени выполнения, я могу посмотреть его, чтобы увидеть, применяется ли vhead.

headOrBust :: LenList a -> Maybe a
headOrBust lla = unLenList lla $ \ n xs -> case n of
  Zy    -> Nothing
  Sy _  -> Just (vhead xs)

Итак, вы смотрите на одно, и при этом узнаете о другом.

Ответ 2

В

fromList :: [a] -> SafeList n a

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

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

Тогда ваша подпись должна быть

fromList :: [a] -> ASafeList a

Вы можете использовать его путем сопоставления шаблонов на ASafeList

useList :: ASafeList a -> ...
useList (ASafeList xs) = ...

и в теле xs будет иметь тип SafeList n a с неизвестным (жестким) n. Вам, вероятно, придется добавить дополнительные операции, чтобы использовать его каким-либо нетривиальным способом.

Ответ 3

Если вы хотите использовать набираемые пользователем функции во время выполнения, вам необходимо убедиться, что эти данные не нарушают закодированные в законах подписи типов. Это проще понять на примере. Вот наша настройка:

data Nat = Z | S Nat

data Natty (n :: Nat) where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

data Vec :: * -> Nat -> * where
  VNil :: Vec a Z
  VCons :: a -> Vec a n -> Vec a (S n)

Мы можем написать некоторые простые функции на Vec:

vhead :: Vec a (S n) -> a
vhead (VCons x xs) = x

vtoList :: Vec a n -> [a]
vtoList  VNil        = []
vtoList (VCons x xs) = x : vtoList xs

vlength :: Vec a n -> Natty n
vlength  VNil        = Zy
vlength (VCons x xs) = Sy (vlength xs)

Для записи канонического примера функции lookup нам понадобится понятие конечных множеств. Обычно они определяются как

data Fin :: Nat -> where
    FZ :: Fin (S n)
    FS :: Fin n -> Fin (S n)

Fin n представляет все числа меньше n.

Но так же, как есть эквивалент уровня типа Nat - Natty s, существует эквивалент уровня типа Fin s. Но теперь мы можем включить уровень и уровень уровня Fin s:

data Finny :: Nat -> Nat -> * where
    FZ :: Finny (S n) Z
    FS :: Finny n m -> Finny (S n) (S m)

Первая Nat является верхней границей a Finny. А второй Nat соответствует фактическому значению a Finny. То есть он должен быть равен toNatFinny i, где

toNatFinny :: Finny n m -> Nat
toNatFinny  FZ    = Z
toNatFinny (FS i) = S (toNatFinny i)

Определение функции lookup теперь прост:

vlookup :: Finny n m -> Vec a n -> a
vlookup  FZ    (VCons x xs) = x
vlookup (FS i) (VCons x xs) = vlookup i xs

И некоторые тесты:

print $ vlookup  FZ               (VCons 1 (VCons 2 (VCons 3 VNil))) -- 1
print $ vlookup (FS FZ)           (VCons 1 (VCons 2 (VCons 3 VNil))) -- 2
print $ vlookup (FS (FS (FS FZ))) (VCons 1 (VCons 2 (VCons 3 VNil))) -- compile-time error

Это было просто, но как насчет функции take? Это не сложно:

type Finny0 n = Finny (S n)

vtake :: Finny0 n m -> Vec a n -> Vec a m
vtake  FZ     _           = VNil
vtake (FS i) (VCons x xs) = VCons x (vtake i xs)

Нам нужно Finny0 вместо Finny, потому что lookup требует, чтобы Vec был непустым, поэтому, если есть значение типа Finny n m, тогда n = S n' для некоторого n', Но vtake FZ VNil совершенно справедливо, поэтому нам нужно расслабиться это ограничение. Таким образом, Finny0 n представляет все числа меньше или равно n.

Но как насчет данных времени выполнения?

vfromList :: [a] -> (forall n. Vec a n -> b) -> b
vfromList    []  f = f VNil
vfromList (x:xs) f = vfromList xs (f . VCons x)

т.е. "Дайте мне список и функцию, которая принимает Vec произвольной длины, и я применим последнюю к первой". vfromList xs возвращает продолжение (т.е. что-то типа (a -> r) -> r) по модулю типов более высокого ранга. Попробуем:

vmhead :: Vec a n -> Maybe a
vmhead  VNil        = Nothing
vmhead (VCons x xs) = Just x

main = do
    print $ vfromList ([] :: [Int]) vmhead -- Nothing
    print $ vfromList  [1..5]       vmhead -- Just 1

Работает. Но разве мы просто не повторяемся? Почему vmhead, когда есть vhead уже? Должны ли мы переписать все безопасные функции небезопасным способом, чтобы можно было использовать их во время выполнения данных? Это было бы глупо.

Нам нужно только убедиться, что все инварианты выполнены. Попробуйте этот принцип в функции vtake:

fromIntFinny :: Int -> (forall n m. Finny n m -> b) -> b
fromIntFinny 0 f = f FZ
fromIntFinny n f = fromIntFinny (n - 1) (f . FS)

main = do       
    xs <- readLn :: IO [Int]
    i <- read <$> getLine
    putStrLn $
        fromIntFinny i $ \i' ->
        vfromList xs   $ \xs' ->
        undefined -- what here?

fromIntFinny аналогичен vfromList. Поучительно видеть, каковы типы:

i'  :: Finny n m
xs' :: Vec a p

Но vtake имеет этот тип: Finny0 n m -> Vec a n -> Vec a m. Поэтому нам нужно принудить i', чтобы он был типа Finny0 p m. А также toNatFinny i' должно быть равно toNatFinny coerced_i'. Но это принуждение вообще невозможно, так как если S p < n, то есть элементы из Finny n m, которые не находятся в Finny (S p) m, так как S p и n являются верхними границами.

coerceFinnyBy :: Finny n m -> Natty p -> Maybe (Finny0 p m)
coerceFinnyBy  FZ     p     = Just FZ
coerceFinnyBy (FS i) (Sy p) = fmap FS $ i `coerceFinnyBy` p
coerceFinnyBy  _      _     = Nothing

Вот почему здесь Maybe.

main = do       
    xs <- readLn :: IO [Int]
    i <- read <$> getLine
    putStrLn $
        fromIntFinny i $ \i' ->
        vfromList xs   $ \xs' ->
        case i' `coerceFinnyBy` vlength xs' of
            Nothing  -> "What should I do with this input?"
            Just i'' -> show $ vtoList $ vtake i'' xs'

В случае Nothing число, которое было считано с ввода, больше, чем длина списка. В случае Just число меньше или равно длине списка и принуждается к соответствующему типу, поэтому vtake i'' xs' хорошо типизирован.

Это работает, но мы ввели функцию coerceFinnyBy, которая выглядит довольно ad hoc. Разрешимым "меньшим или равным" отношением была бы подходящая альтернатива:

data (:<=) :: Nat -> Nat -> * where
    Z_le_Z :: Z :<= m                 -- forall n, 0 <= n
    S_le_S :: n :<= m -> S n :<= S m  -- forall n m, n <= m -> S n <= S m

type n :< m = S n :<= m

(<=?) :: Natty n -> Natty m -> Either (m :< n) (n :<= m) -- forall n m, n <= m || m < n
Zy   <=? m    = Right Z_le_Z
Sy n <=? Zy   = Left (S_le_S Z_le_Z)
Sy n <=? Sy m = either (Left . S_le_S) (Right . S_le_S) $ n <=? m

И безопасная инъекционная функция:

inject0Le :: Finny0 n p -> n :<= m -> Finny0 m p
inject0Le  FZ     _          = FZ
inject0Le (FS i) (S_le_S le) = FS (inject0Le i le)

т.е. если n является верхней границей для некоторого числа и n <= m, то m также является верхней границей для этого числа. И еще один:

injectLe0 :: Finny n p -> n :<= m -> Finny0 m p
injectLe0  FZ    (S_le_S le) = FZ
injectLe0 (FS i) (S_le_S le) = FS (injectLe0 i le)

Теперь код выглядит следующим образом:

getUpperBound :: Finny n m -> Natty n
getUpperBound = undefined

main = do
    xs <- readLn :: IO [Int]
    i <- read <$> getLine
    putStrLn $
        fromIntFinny i $ \i'  ->
        vfromList xs   $ \xs' ->
        case getUpperBound i' <=? vlength xs' of
            Left  _  -> "What should I do with this input?"
            Right le -> show $ vtoList $ vtake (injectLe0 i' le) xs'

Он компилируется, но какое определение должно иметь getUpperBound? Ну, вы не можете определить это. A n в Finny n m живет только на уровне типа, вы не можете его извлечь или получить как-то. Если мы не можем выполнить "downcast", мы можем выполнить "upcast":

fromIntNatty :: Int -> (forall n. Natty n -> b) -> b
fromIntNatty 0 f = f Zy
fromIntNatty n f = fromIntNatty (n - 1) (f . Sy)

fromNattyFinny0 :: Natty n -> (forall m. Finny0 n m -> b) -> b
fromNattyFinny0  Zy    f = f FZ
fromNattyFinny0 (Sy n) f = fromNattyFinny0 n (f . FS)

Для сравнения:

fromIntFinny :: Int -> (forall n m. Finny n m -> b) -> b
fromIntFinny 0 f = f FZ
fromIntFinny n f = fromIntFinny (n - 1) (f . FS)

Таким образом, продолжение в fromIntFinny универсально квантуется по переменным n и m, а продолжение в fromNattyFinny0 универсально квантуется только при m. И fromNattyFinny0 получает Natty n вместо Int.

Существует Finny0 n m вместо Finny n m, потому что FZ является элементом forall n m. Finny n m, а FZ необязательно является элементом forall m. Finny n m для некоторого n, в частности FZ а не элемент forall m. Finny 0 m (поэтому этот тип не заселен).

В конце концов, мы можем присоединиться к fromIntNatty и fromNattyFinny0 вместе:

fromIntNattyFinny0 :: Int -> (forall n m. Natty n -> Finny0 n m -> b) -> b
fromIntNattyFinny0 n f = fromIntNatty n $ \n' -> fromNattyFinny0 n' (f n')

Достижение того же результата, что и в ответе @pigworker:

unLenList :: LenList a -> (forall n. Natty n -> Vec n a -> t) -> t
unLenList (LenList xs) k = k natty xs

Некоторые тесты:

main = do
    xs <- readLn :: IO [Int]
    ns <- read <$> getLine
    forM_ ns $ \n -> putStrLn $
        fromIntNattyFinny0 n $ \n' i' ->
        vfromList xs         $ \xs'   ->
        case n' <=? vlength xs' of
            Left  _  -> "What should I do with this input?"
            Right le -> show $ vtoList $ vtake (inject0Le i' le) xs'

для

[1,2,3,4,5,6]
[0,2,5,6,7,10]

возвращает

[]
[1,2]
[1,2,3,4,5]
[1,2,3,4,5,6]
What should I do with this input?
What should I do with this input?

Код: http://ideone.com/3GX0hd

ИЗМЕНИТЬ

Ну, вы не можете определить его. A n в Finny n m живет только по типу уровень, вы не можете извлечь его или получить как-то.

Это не так. Имея SingI n => Finny n m -> ..., мы можем получить n как fromSing sing.