Не удается уничтожить переходный тип

Question

Say У меня есть следующий GADT:

data Stage a b where 
    Comb :: Stage a b -> Stage b c -> Stage a c 
    FMap :: (a -> b) -> Stage a b 

Теперь я хочу функцию, которая работает следующим образом:

run (a `Comb` b) = (a,b) 
run (FMap f)  = (FMap f,FMap id) 

Как бы построить такую ​​функцию?

Я пробовал разные способы связывания типов, но не удалось. Есть ли расширение, которое у меня отсутствует, что позволяет использовать более обширные привязки типов?

Это сообщение об ошибке:

Couldn't match type `t' with `(Stage t1 b, Stage b t2)' 
    `t' is a rigid type variable bound by 
     the inferred type of run :: Stage t1 t2 -> t at <interactive>:11:5 
In the expression: (a, b) 
In an equation for `run': run (a Comb b) = (a, b) 

Описание того, что я хочу сделать: Я хочу разработать DSL и выполнения функции, которые могут попытаться запустить код из DSL в паре по-разному (у меня есть несколько разных функций запуска для каждого способа). Функция запуска попытается запустить как можно больше кода, предоставленного ему, а затем сообщит, какой код он не может выполнить, и каков результат выполнения кода.

Answer 1

Вам понадобится подпись типа для run, потому что вы используете шаблон для GADT. Согласование шаблонов в GADT требует уточнения типа и, как правило, работает только в том случае, если существует подпись типа.

Но непонятно, что такое подпись типа. Если входное значение

a `Comb` b :: Stage x y 

тогда вы вернетесь (a, b), где

a :: Stage x b 
b :: Stage b y 

неизвестно b. Это экранирование экзистенциального типа. Вы не можете написать

run :: Stage x y -> (State x b, Stage b y) 

, потому что это означало бы, что бы работать для всехb, но он работает только для некоторого (неизвестно) b.

К сожалению, неясно, почему вы хотите написать такую ​​функцию, как run. Зачем производить пару? Что вы хотите сделать с этой парой позже? Comb конструктор определен объединить два этапа, которые имеют неизвестный промежуточный тип, так что эта версия run будет работать:

run :: Stage a b -> Stage a b 
run (a `Comb` b) = a `Comb` b 
run (FMap f)  = FMap f `Comb` FMap id 

Или вы могли бы определить более конкретный тип данных только позволяющий получать «пару» на два этапа с неизвестным промежуточный тип:

data PairStages a b where 
    PairStages :: Stage a b -> Stage b c -> PairStages a c 

И потом:

run :: Stage a b -> PairStages a b 
run (a `Comb` b) = PairStages a b 
run (FMap f)  = PairStages (FMap f) (FMap id) 

Но он все еще чувствует себя странно для меня, что run возвращает пару. Как я уже сказал, непонятно, что вы хотите сделать с результатом run. Казалось бы, более полезно, чтобы run была рекурсивной функцией, которая фактически каким-то образом объединяет результаты запуска компонентов в случае Comb.Например, вот так:

run :: Stage a b -> (a -> b) 
run (a `Comb` b) = run b . run a 
run (FMap f)  = f