Могу ли я принудить экзистенциально квантифицированный аргумент в конструкторе типа?

У меня есть тип данных, чей (единственный) конструктор содержит экзистенциально квантифицированную переменную типа:

data LogEvent = forall a . ToJSON a =>
            LogEvent { logTimestamp     :: Date
                     , logEventCategory :: Category
                     , logEventLevel    :: LogLevel
                     , logThreadId      :: ThreadId
                     , logPayload       :: a
                     }

Когда я изначально писал этот тип, я спрятал полиморфную полезную нагрузку, потому что все, что меня интересовало в то время, это вывод в какой-то файл/поток. Но теперь я хочу заняться более интересными вещами, для которых мне нужно наблюдать за фактическим типом a.

Я понимаю из этот вопрос и другие чтения, которые экзистенциально квантифицируют переменные типа, уникальны при каждом экземпляре. Однако, если задан тип ToJSON a, я могу сделать что-то вроде следующего (псевдокод):

 let x :: Result Foo = fromJSON $ toJSON (logPayload event)

Кажется странным иметь возможность конвертировать в JSON и обратно с более точным типом, хотя я могу понять причину этого.

Итак, как я могу переписать этот тип, чтобы позволить извлекать logPayload, если я знаю его тип? я


types haskell existential-type gadt
person insitu    schedule 16.04.2015    source источник

Ответы (3)


arrow_upward
9
arrow_downward

Это похоже на экзистенциальный класс типов (анти- )шаблон. Эта экзистенциальная магия эквивалентна

data LogEvent = 
        LogEvent { logTimestamp     :: Date
                 , logEventCategory :: Category
                 , logEventLevel    :: LogLevel
                 , logThreadId      :: ThreadId
                 , logPayload       :: Aeson.Value
                 }

но это более четко передает то, что представляет ваша структура. Не стоит ожидать от своей экзистенциальной структуры ничего такого, чего бы вы не ожидали от этого.

С другой стороны, если вы действительно знаете тип logPayload, вам следует закодировать это знание на уровне типа, переместив переменную типа наружу:

data LogEvent a = ...

В этот момент значение типа LogPayload Foo представляет ваши знания о типе полезной нагрузки. Тогда, если вы так склонны, вы могли бы определить

data ALogEvent = forall a. ToJSON a => ALogEvent (LogEvent a)

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

Если вы знаете тип logPayload во время выполнения, но по какой-то причине не можете отслеживать полезную нагрузку во время компиляции, возможно, вы могли бы добавить ограничение Typeable a в свой экзистенциал, чтобы вы могли выполнять приведение, не прибегая к unsafeCoerce... в случае, если вы сделали ошибка, вы не испортите всю свою программу причудливым образом.

person luqui    schedule 16.04.2015
comment
Здесь я использую экзистенциальную оболочку, потому что события передаются по Chan LogEvent для их асинхронного ведения журнала: отдельный поток считывает событие и обрабатывает его. Я, конечно, изначально пытался сделать тип LogEvent параметризованным с его типом полезной нагрузки, но тогда я ничего не получаю, потому что потребитель на другом конце канала все еще не может наблюдать тип события. - person insitu; 16.04.2015
comment
Если потребителю необходимо наблюдать за типом события, я бы рекомендовал алгебраический тип. То есть, если он не обрабатывает все события единообразно, за исключением одного или двух особых случаев, и в этом случае Typeable, вероятно, прав. - person luqui; 16.04.2015
comment
Да, но это означает привязку типа LogEvent к зарегистрированным событиям, чего я хотел избежать, но, очевидно, больше не смогу откладывать :-) Это не библиотечный код, поэтому меня это не слишком волнует, хотя это означает, что модуль журнала зависит на каждом зарегистрированном типе системы, что немного отстойно... - person insitu; 17.04.2015
comment
@insitu, если регистратору необходимо отслеживать тип события, значит, регистратор уже имеет эту зависимость, не так ли? - person luqui; 17.04.2015
comment
Конечно :-) Но не для ВСЕХ зарегистрированных типов. На это вы можете ответить: предоставьте типизированный конструктор для тех типов, которые вам нужно соблюдать, и вы, вероятно, будете правы! Давайте попробуем это... - person insitu; 17.04.2015

arrow_upward
2
arrow_downward

Вы могли бы попробовать дать Data.Typeable шанс; добавьте ограничение Typeable a в свой экзистенциальный тип, а затем, если вы сможете правильно угадать скрытый тип, вы сможете вернуть значение этого типа. См. эту суть в качестве игрушечного примера.

Обратите внимание, что этот метод приносит в жертву некоторую степень безопасности типов — если вы начнете вставлять другой тип внутри LogEvent, которого вы не делали раньше, вы можете нарушить работу пользователей этого типа, которые предполагают, что они успешно обрабатывают каждый подвариант. В отличие от алгебраических типов, динамика и приведения означают, что компилятор не может помочь вам доказать полноту.

person Luis Casillas    schedule 16.04.2015
comment
Следуя комментарию luqui, я начал идти по этому пути, но затем наткнулся на стену: не удается выполнить eta-reduce до экземпляра экземпляра формы (...) => Typeable Command В объявлении экземпляра данных для «Command» Типы, которые я хочу log на самом деле являются экземплярами семейства типов, определенного в классе типов, и кажется, что это DeriveDataTypeable задыхается. Или я могу неправильно интерпретировать ошибки компилятора - person insitu; 17.04.2015

arrow_upward
1
arrow_downward

Итак, как я могу переписать этот тип, чтобы позволить извлекать logPayload, если я знаю его тип?

Если вы не хотите менять свой тип, вы можете заменить fromJSON & toJSON на unsafeCoerce — та же идея, тот же результат, если вы правы, но может привести к сбою вашей программы, если вы не правы в отношении типа.

Если вы хотите, чтобы средство проверки типов удостоверилось, что вы правы, вам придется выставить тип a в LogEvent и не использовать экзистенциальный тип.

person Joachim Breitner    schedule 16.04.2015