проверка целостности с косвенными взаимно рекурсивными типами данных в Idris - PullRequest
Новая
       26

проверка целостности с косвенными взаимно рекурсивными типами данных в Idris

0 голосов
/ 09 декабря 2018

Я работаю с абстрактным синтаксическим деревом, где я хотел бы дать связующим их собственный тип.Кажется, это вызывает проблемы при проверке целостности Идриса ...

С типичной самореференциальной Tree Идрис справляется с проверкой целостности. 

data TreeShape = Last | More TreeShape TreeShape

Show TreeShape where
  show Last = "Leaf"
  show (More left right) = "Branch " ++ show left ++ " " ++ show right

Аналогично со взаимной Tree: 

mutual
  data MuTree = Another MuMuTree
  data MuMuTree = TheLeaf | TheBranch MuTree MuMuTree

  Show MuTree where
    show (Another x) = show x

  Show MuMuTree where
    show TheLeaf = "Leaf"
    show (TheBranch left right) = "Branch " ++ show left ++ " " ++ show right

Но, введите косвенное обращение путем параметризации извлеченного типа, и проверка целостности завершится неудачей: 

data LeftBranch t = L t
(Show t) => Show (LeftBranch t) where
  show (L x) = show x
data TreeOutline = Final | Split (LeftBranch TreeOutline) TreeOutline

Show TreeOutline where
  show Final = "Leaf"
  show (Split left right) = "Branch " ++ show left ++ " " ++ show right

Есть ли способ заставить Idris правильно проверить целостность на рекурсивных типахпоследний сорт?Если не считать этого, есть ли что-то кроме разбрызгивания кода с помощью assert_total s?

...