Как я могу вызвать ошибку типа в Haskell?

Предположим, что у меня есть тип 

data F a = A a | B

Я реализую функцию f :: F a -> F a -> F a следующим образом: 

f (A x) B = A x
f B (A _) = B
f (A _) (A x) = A x

Однако нет такой вещи, как f B B это логически невозможно, поэтому я хочу: 

f B B = GENERATE_HASKELL_COMPILE_ERROR

Что, конечно, не работает. Пропуск определения или использование f B B = undefined не является решением, поскольку создает исключение времени выполнения. Я хотел бы получить ошибку типа времени компиляции.

Компилятор имеет всю информацию, он должен быть в состоянии вывести, что я сделал логическую ошибку. Если сказать я заявляю let z = f (f B (A 1)) B, что должна быть немедленная Ошибка времени компиляции, а не какое-то исключение времени выполнения, которое может скрываться в моем коде в течение многих лет. Я нашел некоторую информацию о контрактах, но я не знаю, как их использовать здесь, и мне интересно, есть ли какой-либо стандартный способ сделать это в Haskell.

EDIT: оказалось, что то, что я пытался сделать, называется зависимым типом, который не полностью поддерживается в Haskell (пока). Тем не менее, можно создать ошибку типа, используя типы индексов и несколько расширений. Решение Дэвида Янга кажется более простым подходом, в то время как Джон Парди творчески использует операторы типов. Я принимаю первое, но мне нравится и то, и другое.

3 4
haskell compile-time

3 ответа:

Это возможно с некоторыми трюками типа, но стоит ли это или нет, зависит от того, что вы делаете (кстати, вы должны предоставить некоторый дополнительный контекст, чтобы мы могли помочь определить, сколько машин типа кажется, что это стоит использовать).

{-# LANGUAGE GADTs           #-}
{-# LANGUAGE TypeFamilies    #-}
{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE ConstraintKinds #-}

import Data.Constraint

data AType
data BType

data F x y where
  A :: a -> F AType a
  B ::      F BType a

type family ValidCombo x y :: Constraint where
  ValidCombo BType ty2 = ty2 ~ AType
  ValidCombo ty1   ty2 = ()

f :: ValidCombo ty1 ty2 => F ty1 a -> F ty2 a -> F ty1 a
f (A x) B     = A x
f B     (A _) = B
f (A _) (A x) = A x

Во время компиляции невозможно сделать определение f B B = ... и невозможно попытаться вызвать его как f B B. Ваш пример let z = f (f B (A 1)) B не будет проверять тип (хотя более сложные примеры могут столкнуться с проблемами).

Первый дело в том, что я добавил дополнительный аргумент в конструктор типа F. Это индекс типа (нигде нет значений этого типа, это просто маркер уровня типа). Я создал два разных пустых типа (AType и BType) для использования в качестве аргументов фантомного типа в F.

Семейство типов

Действует как функция на уровне типов (обратите внимание, что определение очень похоже на определение типичной функции уровня значений Хаскелла, но с типами вместо значений). () - это пустое ограничение, которое никогда не приводит к ошибке типа (поскольку пустое ограничение всегда, тривиально, выполняется). На уровне типа a ~ b ограничивает a и b быть одного типа (~ является равенством уровня типа) и даст ошибку, если они не являются одним и тем же типом. Это примерно аналогично коду уровня значений, который выглядит следующим образом (используя ваш исходный тип F), но на уровне типа: 

data Tag = ATag | BTag
  deriving Eq

getTag :: F a -> Tag
getTag (A _) = ATag
getTag B     = BTag

validCombo :: F a -> F a -> Bool
validCombo B tag2 = (getTag tag2) == ATag
validCombo _ _    = True

(это можно было бы уменьшить, но я оставил "проверку тегов" и явный равенство для более четкого сравнения.)

Вы можете пойти немного дальше с DataKinds, чтобы потребовать, чтобы первый аргумент типа F был либо AType, либо BType, но я не хочу добавлять слишком много лишнего материала (это немного обсуждается в комментариях).

Все это говорит о том, что во многих случаях решение Maybe, которое предоставил @DirkyJerky,-это путь (из-за дополнительной сложности манипуляций на уровне типов).

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

9

Насколько мне известно, "способ Хаскелла" сделать это не вызовет ошибку времени выполнения , а вместо этого вернет Maybe F

Измените сигнатуру f на f :: F a -> F a -> Maybe (F a), и добавьте еще один тип улова: 

f (A x) B = Just $ A x
f B (A _) = Just $ B
f (A _) (A x) = Just $ A x
f B B = Nothing

Компилятор имеет всю информацию

Нет компилятор не обладает всей информацией.

Как насчет того, что пользователь вашей программы решил, что было введено в функцию f, и они выбрали два типа данных B? Что бы а потом что будет? Вы не можете выдать ошибку компиляции после компиляции программы.

4

Вот еще одно решение с семействами типов, которое вы можете найти проще, так как оно просто опирается на Булеву логику.

{-# LANGUAGE DataKinds, GADTs, TypeFamilies, TypeOperators #-}

data F x a where
  A :: a -> F 'True a
  B :: F 'False a

f
  :: ((x || y) ~ 'True)
  => F x a
  -> F y a
  -> F (x || Not y) a

f (A a) B = A a
f B (A _) = B
f (A _) (A a) = A a

----

type family Not a where
  Not 'True = 'False
  Not 'False = 'True

type family a || b where
  'True || 'True = 'True  -- *
  'True || b = 'True
  a || 'True = 'True
  a || b = 'False
Этот случай не нужен, Но я включил его для полноты картины.

Теперь это ошибка типа:

  • возвращает B, где A ожидается, или наоборот
  • включить случай для f B B ("недоступный код")
  • вызов f B B, даже косвенно с чем-то вроде f (f B (A 1)) B
2