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

Настройки. Давайте определим тип данных, представляющий рекурсивные типы данных:

type Var = String
data STerm = SMu Var STerm
           | SVar Var
           | SArrow STerm STerm
           | SBottom
           | STop
   deriving (Show)

то естьt ::= μα. t | α | t → t | ⊥ | ⊤, Обратите внимание, что ⊥ обозначает тип без жителей, а ⊤ обозначает тип со всеми обитателями. Обратите внимание, что(μα. α) = ⊥, поскольку μ являетсянаименее оператор фиксированной точки.

Мы можем интерпретировать рекурсивный тип данных как бесконечное дерево, возникающее в результате многократного развертыванияμα. t вt[α ↦ μα. t], (Для формального описания этого процесса см.http://lucacardelli.name/Papers/SRT.pdfВ Haskell мы можем определить тип ленивых деревьев, которые не имеют µ-связывателей или переменных:

data LTerm = LArrow LTerm LTerm
           | LBottom
           | LTop
   deriving (Show)

и, в обычном Haskell, функция преобразования из одного в другое:

convL :: [(Var, LTerm)] -> STerm -> LTerm
convL _ STop    = LTop
convL _ SBottom = LBottom
convL ctx (SArrow t1 t2) = LArrow (convL ctx t1) (convL ctx t2)
convL ctx (SVar v)
    | Just l <- lookup v ctx = l
    | otherwise = error "unbound variable"
convL ctx (SMu v t) = fix (\r -> convL ((v, r) : ctx) t)

Однако есть проблема с этой функцией: она не продуктивна. Если вы бежитеconvL [] (SMu "x" (SVar "x")) Вы будете бесконечной петлей. Мы бы предпочли получитьLBottom в этом случае. Интересным упражнением является прямое исправление этой функции, чтобы она была продуктивной; Однако в этом вопросе я хочу решить проблему по-другому.

Производительность с модальностью задержки. Когда мы строим циклические структуры данных, как указано выше, нам нужно убедиться, что мы не используем результаты наших вычислений до того, как мы их построим. Модальность задержки - это способ гарантировать, что мы пишем продуктивные (не бесконечные циклы) программы. Основная идея проста: если типInt означает, что у меня есть целое число сегодня, я определяю конструктор типаD, чтобыD Int означает, что у меня есть значение типаInt завтра. D является функтором и аппликативным (но НЕ монадой)

-- D is abstract; you are not allowed to pattern match on it
newtype D a = D a
   deriving (Show)

instance Functor D where
    fmap f (D a) = D (f a)

instance Applicative D where
    D f <*> D a = D (f a)
    pure x = D x

СD, мы определяем оператор с фиксированной точкой: он говорит, что для создания значенияa, вы можете иметь доступ кa вы строите, если вы только используете егозавтра.

fixD :: (D a -> a) -> a
fixD f = f (D (fixD f))

Например, поток состоит из значенияa У меня сегодня и стримStream a который я должен произвести завтра.

data Stream a = Cons a (D (Stream a))

С помощьюfixDЯ могу определитьmap функция на потоках, котораягарантированный быть продуктивным, так как рекурсивный вызовmap используется только для произведенных значений, которые необходимы завтра.

instance Functor Stream where
    fmap f = fixD $ \go (Cons x xs) -> Cons (f x) (go <*> xs)

Эта проблема. Вот вариантLTerm с явной модальностью задержки.

data Term = Arrow (D Term) (D Term)
          | Bottom
          | Top
    deriving (Show)

С помощьюfixD (не допускаются неструктурно-рекурсивные ссылки), как написать функциюconv :: STerm -> Term (или жеconv :: STerm -> D Term)? Особенно интересный тестовый примерSMu "x" (SArrow STop (SMu "y" (SVar "x"))); в результирующей структуре не должно быть никаких Низов!

Обновить. Я случайно исключил структурную рекурсию наSTermчто не было целью вопроса; Я перефразировал это ограничение.