Вопрос по haskell – Почему я не могу использовать селекторы записей с экзистенциально определенным типом?

27

При использовании типов Existential мы должны использовать синтаксис сопоставления с образцом для извлеченияforallред значение. Мы не можем использовать обычные селекторы записей в качестве функций. GHC сообщает об ошибке и предлагает использовать сопоставление с шаблоном с этим определениемyALL:

<code>{-# LANGUAGE ExistentialQuantification #-}

data ALL = forall a. Show a => ALL { theA :: a }
-- data ok

xALL :: ALL -> String
xALL (ALL a) = show a
-- pattern matching ok

-- ABOVE: heaven
-- BELOW: hell

yALL :: ALL -> String
yALL all = show $ theA all
-- record selector failed
</code>
<code>forall.hs:11:19:
    Cannot use record selector `theA' as a function due to escaped type variables
    Probable fix: use pattern-matching syntax instead
    In the second argument of `($)', namely `theA all'
    In the expression: show $ theA all
    In an equation for `yALL': yALL all = show $ theA all
</code>

Некоторые из моих данных занимают более 5 элементов. Трудно поддерживать код, если я использовать сопоставление с шаблоном:

<code>func1 (BigData _ _ _ _ elemx _ _) = func2 elemx
</code>

Есть ли хороший способ сделать такой код обслуживаемым или обернуть его так, чтобы я мог использовать какие-то селекторы?

Подсказка: какой бы типtheA? Louis Wasserman
Или, точнее, это будет иметь типexists a. Show a => ALL -> aУ Haskell были первоклассные экзистенциальные типы. javawizard
В основном ответ таков:doesn't имеет выражаемый тип, поэтому вам нужно сопоставление с образцом, чтобы получить работоспособный тип. Louis Wasserman
@ Луис Вассерман: Вы имеете в виду использование экзистенциального синтаксиса в yALL? как? Nybble

Ваш Ответ

2   ответа
16

func1 BigData{ someField = elemx } = func2 elemx

работает и намного меньше печатает для огромных типов.

Отличный ответ! Я нашел это позже: data B {x :: Int, y :: Int}; fun B {..} = x + y; это может быть альтернативой. Nybble
18

чем обычные типы. GHC (справедливо) запрещает вам использоватьtheA как функция. Но представьте, что такого запрета не было. Какой тип будет иметь эта функция? Это должно быть что-то вроде этого:

-- Not a real type signature!
theA :: ALL -> t  -- for a fresh type t on each use of theA; t is an instance of Show

Говоря очень грубо,forall заставляет GHC "забыть" тип аргументов конструктора; все, что система типов знает, это то, что этот тип является экземпляромShow, Поэтому, когда вы пытаетесь извлечь значение аргумента конструктора, невозможно восстановить исходный тип.

За кулисами GHC делает то, что говорится в комментарии к фиктивной сигнатуре выше, каждый раз, когда вы сопоставляете шаблон сALL конструктор, переменной, связанной со значением конструктора, назначается уникальный тип, который гарантированно отличается от любого другого типа. Возьмите для примера этот код:

case ALL "foo" of
    ALL x -> show x

Переменнаяx получает уникальный тип, который отличается от любого другого типа в программе и не может быть сопоставлен ни с какой переменной типа. Этим уникальным типам не разрешается выходить на верхний уровень & # x2014; именно поэтомуtheA не может быть использован как функция.

+1 Это объясняет сообщение об ошибке "Невозможно использовать селектор записей" theA "; как функцияdue to escaped type variables& Quot;
Как правило, вы можете думать о экзистенциальном типе как о зависимом кортеже, где первый элемент является типом (*) и второе значение этого типа -Σ[ a : * ] a, Проблема в том, что когда вы пытаетесь написать сигнатуру типа для проекции второго элемента кортежа, вам необходимо знать значение первого элемента. Это не может быть выражено в Haskell. Если у вас есть язык с независимой типизацией, вы можете написать его (используя нотацию Agda):(x : Σ[ a : * ] a) → fst x.

Похожие вопросы