作为 Term 或 Value 计算结果的返回类型

Question

我试图很好地掌握种类、类型和术语（或值，不确定哪个是正确的）以及用于操作它们的 GHC 扩展。我知道我们可以使用 TypeFamilies 来编写带有 Types 的函数，现在我们还可以在某种程度上使用 DataKinds、PolyKinds 等来操作 Kinds。我已经阅读了关于 Singleton Types 的 paper 这似乎很有趣，尽管我还没有完全理解它.这一切都让我想知道，有没有一种方法可以创建一个基于 Term 或 Value 级别的计算来计算返回类型的函数？这是依赖类型实现的吗？

这是我的想法的一个例子

data Type1
data Type2

f :: Type1 -> Type2 -> (Type1 or Type2)--not using Either or some "wrapper" ADT

--更新--------

基于这里的大量研究和帮助，我现在很清楚，无论我启用多少扩展，函数的返回类型永远无法根据 Haskell 中的值级别的表达式来计算。所以我发布了更多我的实际代码，希望有人能帮助我决定前进的最佳方式。我正在编写一个以圆锥曲线和二次曲面为基本类型的小型库。对这些类型的操作涉及计算它们之间的交集。 2个曲面的交点是圆锥曲线的一种类型，包括像点一样的退化（实际上除了圆锥之外还需要另一种类型的曲线，但除了点之外）。确切的曲线返回类型只能由运行时相交曲面的值确定。圆柱体 - 平面相交可以产生无、直线、圆或椭圆。 我的第一个计划是像这样使用 ADT 来构造曲线和曲面......

data Curve = Point     !Vec3
           | Line      !Vec3 !UVec3
           | Circle    !Vec3 !UVec3 !Double
           | Ellipse   !Vec3 !UVec3 !UVec3 !Double !Double
           | Parabola  !Vec3 !UVec3 !UVec3 !Double
           | Hyperbola !Vec3 !UVec3 !UVec3 !Double !Double
           deriving(Show,Eq)

data Surface = Plane    !Vec3 !UVec3
             | Sphere   !Vec3 !Double
             | Cylinder !Vec3 !UVec3 !Double
             | Cone     !Vec3 !UVec3 !Double
             deriving(Show,Eq)

...这是最直接的，并且具有很好的封闭代数类型的优点，我喜欢。在这种表示中，交集的返回类型很简单，它只是曲线。这种表示的缺点是这些类型的每个函数都必须为每种类型进行模式匹配并处理所有排列，这对我来说似乎很麻烦。 Surface-Surface 相交函数将有 16 个图案进行匹配。

下一个选项是让每个 Surface 和 Curve 类型保持独立。像这样，

data Point     = Point     !Vec3                               deriving(Show,Eq)
data Line      = Line      !Vec3 !UVec3                        deriving(Show,Eq)
data Circle    = Circle    !Vec3 !UVec3 !Double                deriving(Show,Eq)
data Ellipse   = Ellipse   !Vec3 !UVec3 !UVec3 !Double !Double deriving(Show,Eq)
data Parabola  = Parabola  !Vec3 !UVec3 !UVec3 !Double         deriving(Show,Eq)
data Hyperbola = Hyperbola !Vec3 !UVec3 !UVec3 !Double !Double deriving(Show,Eq)


data Plane    = Plane    !Vec3 !UVec3                          deriving(Show,Eq)
data Sphere   = Sphere   !Vec3 !Double                         deriving(Show,Eq)
data Cylinder = Cylinder !Vec3 !UVec3 !Double                  deriving(Show,Eq)
data Cone     = Cone     !Vec3 !UVec3 !Double                  deriving(Show,Eq)

从长远来看，这似乎更灵活，并且很好且细化，但需要包装器 ADT 才能处理来自交集函数的多种返回类型或构建一般“曲线”列表或“表面”是因为它们之间没有关系。我可以使用类型类和存在来对它们进行分组，但是我失去了我不喜欢的原始类型。

这些设计中的妥协让我尝试了这个..

---------------------------------------------------------------
-- Curve Types
---------------------------------------------------------------
type Pnte = Curve PNT
type Line = Curve LIN
type Circ = Curve CIR
type Elli = Curve ELL
type Para = Curve PAR
type Hype = Curve HYP
-----------------------------------------------
data CrvIdx = PNT
            | LIN
            | CIR
            | ELL
            | PAR
            | HYP
-----------------------------------------------
data Curve :: CrvIdx → * where 
  Pnte :: !Vec3                                       → Curve PNT
  Line :: !Vec3 → !UVec3                              → Curve LIN
  Circ :: !Vec3 → !UVec3 → !Double                    → Curve CIR
  Elli :: !Vec3 → !UVec3 → !UVec3 → !Double → !Double → Curve ELL
  Para :: !Vec3 → !UVec3 → !UVec3 → !Double           → Curve PAR
  Hype :: !Vec3 → !UVec3 → !UVec3 → !Double → !Double → Curve HYP

---------------------------------------------------------------
-- Surface Types
---------------------------------------------------------------
type Plne = Surface PLN
type Sphe = Surface SPH
type Cyln = Surface CYL
type Cone = Surface CNE
-----------------------------------------------
data SrfIdx = PLN
            | SPH
            | CYL
            | CNE 
-----------------------------------------------
data Surface :: SrfIdx → * where
  Plne :: !Vec3 → !UVec3           → Surface PLN
  Sphe :: !Vec3 → !Double          → Surface SPH
  Cyln :: !Vec3 → !UVec3 → !Double → Surface CYL
  Cone :: !Vec3 → !UVec3 → !Double → Surface CNE

...起初我认为这会给我一些神奇的，两全其美的场景，我可以通过“曲线”引用任何曲线类型（如在列表或交集返回类型中）并且还有可用的完整类型 (Curve CrvIdx) 以使用多参数类型类等以粒度样式编写函数。我很快发现这并不像我希望的那样工作得很好，正如question 中所示。我一直顽固地继续用头撞墙，试图找到一种方法来编写一个函数，该函数可以根据运行时参数的几何属性从我的 GADT 中选择返回类型，现在意识到这不会发生。所以现在的问题是什么是表示这些类型以及它们之间的交互的有效和灵活的方式？谢谢。

Answer 1

简短的回答：不。您需要使用包装器 ADT、Data.Dynamic 或 type-family/associated type。

类型族可能是最接近您想要的，但同样， 类型需要能够在编译时确定。例如：

{-# LANGUAGE TypeFamilies #-}

data Red
data Green
data Blue

data Yellow
data Cyan
data Violet

type family MixedColor a b
type instance MixedColor Red Red      = Red
type instance MixedColor Red Green    = Yellow
type instance MixedColor Red Blue     = Violet
type instance MixedColor Green Red    = Yellow
type instance MixedColor Green Green  = Green
type instance MixedColor Green Blue   = Cyan
-- etc ..

mixColors :: c1 -> c2 -> MixedColor c1 c2
mixColors = undefined

这里，mixColors 函数基本上可以返回任何类型的值， 但返回类型需要是类型族MixedColor 的一个实例 这样编译器就可以根据参数类型推断出实际的返回类型。

您可以使用类型族和类型类来构建相对复杂的 类型函数，让你越来越接近依赖的功能 类型，但这意味着您的数据需要使用足够的类型级别进行修饰 进行所需类型计算的信息。

如果您需要编码，最近引入的type-level natural numbers 会很有用 类型中的数值计算。

编辑：另外，我不确定您为什么不愿意使用 ADT（也许您需要更详细地描述您的用例？），因为编码例如一个函数可以返回Type1 或Type2 的事实正是ADT 非常自然地编码并且惯用的那种信息。