Каковы правила для типов уникальности в Идрисе? - PullRequest
Новая
       54

Каковы правила для типов уникальности в Идрисе?

0 голосов
/ 27 февраля 2020

В документации Idris упоминается, что значение с типом UniqueType не может быть упомянуто дважды при сопоставлении с образцом, например: 

data UList : Type -> UniqueType where
     Nil   : UList a
     (::)  : a -> UList a -> UList a
dupList : UList a -> UList a
dupList xs = xs ++ xs

Через несколько строк оно упоминается, что этот код: 

showU : Show a => UList a -> String
showU xs = "[" ++ showU' xs ++ "]" where
  showU' : UList a -> String
  showU' [] = ""
  showU' [x] = show x
  showU' (x :: xs) = show x ++ ", " ++ showU' xs

использует список, поэтому его нельзя использовать впоследствии, например, в: 

printAndUpdate : UList Int -> IO ()
printAndUpdate xs = do putStrLn (showU xs)
                       let xs' = umap (*2) xs -- xs no longer available!
                       putStrLn (showU xs')

Но как мне это оправдать? Разве две ссылки в последовательности операций (не только в сопоставлении с образцом) также запрещены?

...