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

Question

Я очень заинтересован в компиляции 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 добился хорошего прогресса в направлении зависимого типа, поэтому мне интересно: есть ли способ написать функции, которые возвращают разные типы на основе входного значения?

Answer 1

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

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

Answer 2

GADTs + 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), если планируете делать такие вещи повсеместно. Поисковый термин, который вы хотите увидеть, чтобы увидеть больше примеров такого рода хакерских атак, - это «синглтон-типы», часто сокращенно называемые просто «синглтоны».

Answer 3

Возможно, стоит отметить, что на практике библиотеку 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.