Как написать функцию from и to для Add Void a === a?

Из документа: http://chris-taylor.github.io/blog/2013/02/10/the-алгебра-оф-алгебраических-данных-типов/, там написано:

Bool и Add () () эквивалентны, потому что мы можем определить функцию «от» и «до»:

to :: Bool -> Add () ()
to False = AddL ()
to True  = AddR ()

from :: Add () () -> Bool
from (AddL _) = False
from (AddR _) = True

Это:

from (to a) == a
to (from a) == a

Затем он дает еще два:

 Add Void a === a
 Add a b === Add b a

Как написать функции «от» и «до» для этих двух?


haskell algebraic-data-types
person Freewind    schedule 01.08.2014    source источник

Ответы (2)


arrow_upward
5
arrow_downward

Для

Добавить б === Добавить б а

вам нужно поменять местами конструкторы AddL/AddR следующим образом:

to :: Add a b -> Add b a
to (AddL x) = AddR x
to (AddR x) = AddL x

-- from = to

Для

Добавить пустоту a === a

вам нужна полиморфная функция void : Void -> a

to :: Add Void a -> a
to (AddL impossible) = void impossible
to (AddR x) = x

from :: a -> Add Void a
from x = AddR x

Переменная impossible обозначает "несуществующее" значение типа Void. Такого значения действительно нет (кроме дна/неопределенности). Вот почему линия

to (AddL impossible) = ...

на самом деле недостижимый код - он никогда не будет выполнен.

Функция void использует тот факт, что для получения значения a из воздуха требуется невозможный аргумент. К сожалению, в Haskell void нельзя определить, если только не использовать неопределенность, например.

void :: Void -> a
void _ = error "This will never be reached"

Более элегантным и правильным решением было бы

void :: Void -> a
void x = case x of
           -- no constructors for Void, hence no branches here to do!
           -- since all these (zero) branches have type `a`, the whole
           -- case has type `a` (!!!)

но, увы, Haskell запрещает пустые конструкции case. (В GHC 7.8 пустые регистры разрешены через EmptyCase, как указывает bheklilr).

Для сравнения, в языке с зависимой типизацией, таком как Coq или agda, приведенный выше код (с небольшими изменениями) был бы в порядке. Вот это в Coq:

Inductive Void : Set := .   (* No constructors for Void *)

Definition void (A : Set) (x : Void) : A :=
      match x with
      end .

А в Агде

data Void : Set where
   -- no constructors

void : (A : Set) -> Void -> A
void A ()         
-- () is an "impossible" pattern in Agda, telling the compiler that this argument
-- has no values in its type, so one can omit the definition entirely.
person chi    schedule 01.08.2014
comment
но, увы, Haskell запрещает пустые конструкции case. Больше нет, в версии 7.8 теперь есть EmptyCase extension, в котором приводится пример специально для Void. - person bheklilr; 01.08.2014
comment
Я пытался позвонить to (AddL 1), но он сообщает: No instance for (Num a0) arising from the literal 1, The type variable a0' is ambiguous`. Как я могу дать ему правильный параметр? - person Freewind; 01.08.2014
comment
@Freewind Используйте to (AddL (1::Int)), чтобы указать тип для 1. Haskell жалуется, потому что контекст вокруг 1 не позволяет понять, должно ли 1 быть Int, Double или любым другим числовым типом. - person chi; 01.08.2014

arrow_upward
4
arrow_downward

В библиотеке void есть absurd с типом Void -> a. Он отражает логический принцип «из ложного все следует».

Его можно использовать для удаления ветви Void из типов суммы. Интуитивно, если ваш тип либо a, либо что-то невозможное, то это почти то же самое, что и a.

import Data.Void

foo :: Either Void a -> a
foo x = either absurd id x
person danidiaz    schedule 01.08.2014