«Свободные» переменные типа, связанные с помощью функциональных зависимостей в синонимов типа

Question

Учитывая класс

class MonadSignal m sigs | m -> sigs where ... 

и класс

class CanSignal sigs sigs' where ... 

Я хочу, чтобы определить синоним типа, как этот

type MonadSignal' sigs m = (MonadSignal m sigs', CanSignal sigs sigs') 

Здесь переменная sigs' не упоминается в заголовке синонима типа MonadSignal', но она там только для того, чтобы соединить первое и второе ограничение, и оно однозначно определяется m, которое - это, упомянутое в голове.

Обычно я думаю, что я был бы в состоянии forall его на РИТ, но так как это просто Constraint синоним, нет никакого фактического тела для переменной появляться в.

Можно что-нибудь сделать здесь? (К тому же положить переменную в голову и дает неправильное впечатление, когда синоним фактически используется, что это фактическая «переменная»)

Answer 1

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

{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE FlexibleContexts #-} 
{-# LANGUAGE ConstraintKinds #-} 
{-# LANGUAGE TypeFamilies #-} 
module TypeFamily where 

class Monad m => MonadSignal m where 
    type Sig m :: * 
    make :: m sig 

class CanSignal sigs sigs' where 

type MonadSignal' sigs m = (MonadSignal m, CanSignal sigs (Sig m)) 

Это, возможно, не совсем так хороша, как с помощью классов типа многопараметрических для обоих, но это должно быть так же, как эквивалент в выразительности, и вам не придется беспокоиться о выполнении этого «транзитивное замыкание» Такие вещи.

Answer 2

Вы можете заменить синоним типа с классом:

class MonadSignal' sigs (m :: * -> *) 
instance (MonadSignal m sigs', CanSignal sigs sigs') => MonadSignal' sigs m 

В класса, переменная типа sigs' не отображается в заголовке класса, , поэтому для этого вам необходимо использовать {-# LANGUAGE UndecidableInstances #-}. Хотя я не считаю, что этот класс может фактически привести к прекращению.

Answer 3

К сожалению, я считаю, что вы должны дать это неправильное впечатление, если настаиваете на правильном финансировании (см. Нижнюю часть этого ответа, если вы примете несколько иной подход). Я кратко подумал, что, возможно, вы могли бы сделать класс MonadSignal', но вы не смогли бы дать ему ограничение суперкласса, которое вы хотите. Вы могли бы наверстать упущенное, если бы я был откровен с одним или несколькими методами Dict, но тогда вашей жизни будет сложно.

Хотя это не имеет отношения, это, вероятно, лучше, чтобы определить

class MonadSignal sigs m | m -> sigs 

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

---

Там еще один способ использования семьи типа, на основе законного осуществления fundeps в терминах семейств типа:

class (sigs ~ Sigs m) => MonadSignal sigs m where 
    type Sigs m :: * -- Or appropriate kind 
    ... 

type MonadSignal' sigs m = (MonadSignal (Sigs m) m, CanSignal sigs (Sigs m))