作为术语或值计算的结果返回类型

Question

我试图很好地理解种类，类型&术语（或值，不知道哪个是正确的）以及用于操作它们的GHC扩展。我知道我们可以使用TypeFamilies来使用Types来编写函数，现在我们也可以在一定程度上使用DataKinds，PolyKinds等操作Kinds。我已经阅读了关于Singleton Types的这个paper，虽然我还没有完全理解，但它似乎很有趣。这一切都让我产生疑惑，是否有办法创建一个函数来计算基于期限或价值水平计算的回报类型？这是依赖类型实现的吗？

这里的基础上研究了很多我在想什么

data Type1 
data Type2 

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

--update --------

一个例子，在这里帮助，它现在已经成为我清楚无论启用了多少个扩展，函数的返回类型都不能根据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个模式匹配。

下一个选项是保持每个曲面和曲线类型不同。像这样，

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能够从交叉功能处理多个返回类型，或建立一个一般“曲线”或“曲面”的列表，因为它们之间没有关系。我可以使用Type Classes和Existentials将它们分组，但是然后我失去了原来的类型，我不喜欢它。

在这些设计中的妥协使我试试这个..

--------------------------------------------------------------- 
-- 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编码非常自然且常用的信息种类。