作爲術語或值計算的結果返回類型

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編碼非常自然且常用的信息種類。