Test case for recursive instantiation

[nponeccop]

Непонятно, зачем рекурсия в функции:

renameVarsInExpr :: Expr -> Infer Expr
renameVarsInExpr x = flip cataM x $ \case
      ExprTypeF tp -> ExprType <$> renameVars vars tp
      x -> return $ embed x
    where
    vars = flip cata x $ \case
        ExprTypeF tp -> setToList $ ftv tp
        x -> ffold x

oczor/src/Oczor/Infer/State.hs

Line 68 in 1b36249

renameVarsInExpr :: Expr -> Infer Expr

Функцию почти не трогали, разве что Fix/unfix заменили на embed/project. Однако она на первый взгляд не имеет смысла - алгоритму W такой обход не требуется.

Замена на более логичный вариант не приводит к падению тестов.

renameVarsInExpr :: Expr -> Infer Expr
renameVarsInExpr (ExprType tp) = ExprType <$> renameVars vars tp where
   vars = setToList $ ftv tp

renameVarsInExpr x = return x

Как понять задумку исходного рекурсивного обхода? Или придумать тест кейс чтобы второй вариант упал?

[sirikid]

На мой неискушенный взгляд похоже на говнокод, особенно куча разных переменных с именем x.

[nponeccop]

Классика хаскеля же. Однобуквенные локальные идентификаторы.

[nponeccop]

Upd: Этот код вообще вызывается только из одного места, где он логически не нужен

oczor/src/Oczor/Infer/Infer.hs

Line 39 in 14dfe83

(Function param guard body) <- renameVarsInExpr ast

И комментирование его там тоже не приводит к падению тестов. Похоже что можно просто удалить саму функцию и её вызов

[ptol]

Похоже просто дублирование. Так как реализация ftv уже рекурсивно проходит по TypeExpr и собирается все TypeVar, то проходить рекурсивно еще раз смысла нет.

[ptol]

На мой неискушенный взгляд похоже на говнокод, особенно куча разных переменных с именем x.

Синтаксис Хаскеля не позволяет избавить от переменных в которых нет необходимости.
Например в oczor case синтаксически просто список функций, поэтому можно заменить

case
  ExprTypeF tp -> setToList $ ftv tp
  x -> ffold x

на

case
  ExprTypeF tp -> setToList $ ftv 
  ffold

[ptol]

Этот код вообще вызывается только из одного места, где он логически не нужен

Это на случай если внутри функции будет описание типа с TypeVar который уже есть в контексте.

[nponeccop]

Так это нормально. Называется (в пейпере Карделли который я сейчас не могу найти) non-generic type variables. Они связаны наружным forall и их "освобождать" нельзя.

В любом случае нужен тест! Ниже аналоги в HNC:

https://github.com/nponeccop/HNC/blob/master/hn_tests/comp-2.hn
https://github.com/nponeccop/HNC/blob/master/hn_tests/comp-2.cpp

Короче тебе задание придумать тест, который упадёт после комментирования renameVarsInExpr. Я там трогать не буду сейчас.