Как создать хорошо типизированную функцию, которая возвращает два разных типа?

Я очень заинтересован в компиляции модулей Formality-Core в библиотеки Haskell. Хотя я мог бы использовать unsafeCoerce везде, было бы интереснее, если бы я мог сохранить информацию о типе, позволяя публиковать скомпилированные модули в Cabal и использовать их в других проектах Haskell. Проблема в том, что зависимые типы позволяют использовать программы, запрещенные Haskell. Например, функция foo ниже:

foo: (b : Bool) -> If(b)(Nat)(Bool)
  (b)
  b<(b) If(b)(Nat)(Bool)>
  | zero;
  | false;

Возвращает другой тип в зависимости от ввода. Если ввод false, он возвращает число zero. Если на входе true, возвращается логическое значение false. Похоже, что подобную функцию нельзя перевести на Haskell. Я считаю, что за последние годы Haskell добился хорошего прогресса в направлении зависимых типов, поэтому мне интересно: есть ли способ написать функции, которые возвращают разные типы на основе входного значения?


haskell dependent-type
person MaiaVictor    schedule 15.04.2020    source источник
comment
Несмотря на достигнутый прогресс, одной ключевой функции зависимых типов — способности компилятора просматривать значения во время компиляции — по-прежнему не хватает. Чтобы выразить это в Haskell, вам нужно либо подтянуть параметр b: Bool к уровню типа, чтобы он был известен во время компиляции, либо, наоборот, подтянуть результирующий тип к уровню значения.   -  person Fyodor Soikin    schedule 15.04.2020
comment
Вам нужна монада Either?   -  person bug_spray    schedule 15.04.2020
comment
Я бы избегал unsafeCoerce, если только другой вариант не работает. У нас есть GADT + синглтоны для имитации некоторых зависимых типов. У нас также есть Dynamic, который выполняет проверку типов во время выполнения, если статический подход не работает. Возможно, существуют другие безопасные варианты.   -  person chi    schedule 15.04.2020
comment
@chi Я нахожу подход одиночек в ответах очень интересным, поскольку он допускает некоторую зависимость, но, оглядываясь назад, я чувствую, что он будет недостаточно мощным для представления произвольных зависимых функций. Так что я не очень уверен, как поступить. Возможно, единственная жизнеспособная альтернатива - просто скомпилировать все в HOAS DSL, но я думаю, что мы потеряем много собственной производительности, сделав это...   -  person MaiaVictor    schedule 15.04.2020
comment
@bug_spray Нет, это не так. Either позволяет только значению вывода зависеть от входного значения, поскольку Left 0 и Right False имеют один и тот же тип, а именно Either Natural Bool. Речь идет о том, чтобы тип вывода зависел от входного значения. (И даже если бы это было так, тот факт, что это монада, не имеет значения. Вы не должны называть вещи монадами только потому, что они имеют экземпляр Monad, если только вы на самом деле каким-то образом не ссылаетесь на экземпляр или не используете его.)   -  person Joseph Sible-Reinstate Monica    schedule 15.04.2020

Ответы (3)


arrow_upward
7
arrow_downward

Современным остается одноэлементный подход.

data SBool b where
  SFalse :: SBool 'False
  STrue :: SBool 'True

type family If (b :: Bool) (t1 :: k) (t2 :: k) :: k where
  If 'False x _ = x
  If 'True _ y = y

foo :: SBool b -> If b Natural Bool
foo SFalse = 0
foo STrue = False
person dfeuer    schedule 15.04.2020

arrow_upward
6
arrow_downward

Примерно это могут сделать GADT + TypeFamilies (опционально + DataKinds). Так:

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

data GADTBool a where
    GADTFalse :: GADTBool False
    GADTTrue :: GADTBool True

type family If cond t f where
    If False t f = f
    If True  t f = t

foo :: GADTBool b -> If b Int Bool
foo GADTTrue = 0
foo GADTFalse = False

Конечно, вы, вероятно, действительно захотите foo :: GADTBool b -> If b (GADTInt 0) (GADTBool False), если вы планируете делать такие вещи повсеместно. Поисковый запрос, по которому вы хотите увидеть больше примеров такого рода хакерских атак, — это «типы синглтонов», часто сокращенно просто «синглтоны».

person Daniel Wagner    schedule 15.04.2020

arrow_upward
3
arrow_downward

Возможно, стоит отметить, что с практической точки зрения библиотека singletons может использоваться для обработки большей части шаблонного кода. Итак, вы можете написать:

{-# LANGUAGE GADTs #-}

module Formality where

import Numeric.Natural
import Data.Singletons.Prelude

foo :: SBool b -> If b Bool Natural
foo SFalse = 0
foo STrue = False

используя почти точно такой же синтаксис, как @dfeuer, вплоть до порядка аргументов до If.

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

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

person Community    schedule 15.04.2020