Там разве нельзя записать тип функции вместо
quot? Тогда и проверку компилятор мог бы делать. Скажем как-нибудь так это могло бы выглядеть:
twice ( a ( a -- a ) -- a ). Посмотрите стековые эффекты
compose и
call — если они не встроены в механизм вывода и язык достаточно выразительный по части типов (вроде до такой степени уж должен был быть, когда я смотрел несколько лет назад), то можно будет увидеть, как выразить это. Тогда компилятор сможет убедиться без инлайна (что на мой взгляд не лучшее решение — инлайн должен бы быть одним, а отмена проверки типов на месте — другим, не связанным маркером).
На хаскеле этот тип выглядел бы
(a ::: s -> a ::: s) ::: a ::: s -> a ::: s, хотя можно и проще:
(s -> s) ::: s -> s. Вышенаписанному эффекту отвечает первый, а не второй, но самому определению отвечает именно что более общий второй; действительно,
Munin как раз замечает, что функция может брать не один аргумент и возвращать тоже не один, в частности ей можно и ноль, и два и т. д., и определению это всё не противоречит, лишь бы она только складывала назад значения тех же типов что брала.
По поводу нотации и всего остального см. демонстративный модуль, который должен компилироваться в GHC. ↓ Если только нет опечаток.
{-# language TypeOperators #-}
import Control.Category ((>>>)) -- композиция слева направо
-- определим гетерогенный cons, который будем писать навроде e1 ::: e2 ::: e3 ::: tail
data top ::: below = top ::: below deriving (Eq, Show)
infixr 5 ::: -- правоассоциативный и достаточно хваткий для удобства чтения кода
-- для дна стека можно использовать хоть и (), но оно нам не понадобится
-- ( a b -- c d ) записывается как тип b ::: a ::: below -> d ::: c ::: below:
-- b ложили последним, вот оно и в голове;
-- `below` — тоже переменная, названная так для понятности,
-- она обозначает неизменный низ стека
-- сии функции предполагаются уже определёнными где-то там,
-- но я приведу и определения чтобы можно было поиграть;
dup :: a ::: below -> a ::: a ::: below
dup (x ::: xs) = x ::: x ::: xs
call :: (stack1 -> stack2) ::: stack1 -> stack2
call (f ::: xs) = f xs
compose :: (stack2 -> stack3) ::: (stack1 -> stack2) ::: below -> (stack1 -> stack3) ::: below
compose (g ::: f ::: xs) = (f >>> g) ::: xs
-- интересующая функция:
twice = dup >>> compose >>> call
-- должен выводиться тип (stack -> stack) ::: stack -> stack
-- его можно унифицировать с предлагавшимся мной выше типом (a ::: s -> a ::: s) ::: a ::: s -> a ::: s
-- Сб дек 28, 2019 02:49:18 --Ну чего, я сам полез смотреть. И:
• Псевдоцитирование действительно есть, ну может разве не такое как я думал:
https://docs.factorcode.org/content/article-fry.html.
• Типы хитренькие вроде всё же есть.
https://docs.factorcode.org/content/article-effects-variables.html, правда я бы не называл это row polymorphism, обычно то немного другое означает (неупорядоченные наборы типов, снабжённых метками, а тут упорядоченные и не снабжённые метками; и используются такие строки для определения extensible records и variants — а тут просто гетерогенный список, ей-диэдру).
george66, попробуйте вашей функции приделать
( ..a quot: ( ..a -- ..a ) -- ..a ), если я правильно понял.
элементов, где 
- верхний элемент стека, а кладёт обратно 
?