在Haskell中使用整數參數化類型

我正在嘗試製作一些Haskell類型，這些類型不是通過類型而是通過類型的元素（特別是整數）進行參數化。例如，R^2中的（線性代數）向量和R^3中的向量是不同類型的對象。具體來說，我正在Haskell編寫一個K-D樹，我想用正整數參數化我的數據結構，因此三維樹和四維樹具有不同的類型。在Haskell中使用整數參數化類型

我試圖通過元組來參數化我的樹，但它似乎沒有去任何地方（似乎有點不太可能這可以通過，特別是因爲它似乎並不是三倍或更大的東西甚至函子（我不知道有什麼辦法說喜歡，例如HomogeneousTuple A =>函子一）我想要做這樣的事情：

data (TupleOfDoubles a) => KDTree a b = ... ---so in a 3DTree a is (Double,Double,Double)

那將是很好的，或者類似的東西，這將是同樣好

data KDTree Int a = ... -- The Int is k, so KDTree has kind Int -> * -> *

有沒有人知道這些效果是可行還是合理？

感謝 -Joseph

來源

2011-09-01 Joseph Victor

一個側面說明，你可能會對一些關於依賴類型的文獻感興趣，它是從值到類型的更一般的函數：我喜歡http://www.cse.chalmers.se/~peterd /papers/DependentTypesAtWork.pdf –

感謝Amos，這似乎是我可以使用的東西 –

有一個GHC擴展名爲TypeNats正在制定，這將是你想要什麼。然而，根據the ticket，目前這個里程碑的設定爲7.4.1，所以這仍然有點兒等待。

在該擴展程序可用之前，您唯一能做的就是使用類型對維度進行編碼。例如沿着這些路線的東西可能的工作：

{-# LANGUAGE ScopedTypeVariables #-} 
class MyTypeNat a where 
    toInteger :: a -> Integer 

data Zero 
data Succ a 

instance MyTypeNat Zero where 
    toInteger _ = 0 

instance MyTypeNat a => MyTypeNat (Succ a) where 
    toInteger _ = toInteger (undefined :: a) + 1 

data KDTree a b = -- ... 

dimension :: forall a b. MyTypeNat a => KDTree a b -> Integer 
dimension = toInteger (undefined :: a)

像這樣的方法的缺點是當然，你必須寫類似KDTree (Succ (Succ (Succ Zero))) Foo而不是KDTree 3 Foo的。

來源

2011-09-01 07:38:17 sepp2k

當然，但是一個類型三= Succ（Succ（Succ Zero））將會有所幫助。 – Ingo

Nifty，謝謝（這有點愚蠢，但我實際上是在挖） –

如果你只打算使用小數字，你可能還想直接對它們進行編碼：數據一/數據二/數據三/數據四 - 它是更容易閱讀。 – firefrorefiddle

sepp2k的答案顯示了這樣做的基本方法。事實上，很多工作已經完成。

類型級包數

自然數的東西使用類型級編碼（實施例）

遺憾的是這樣的：

data KDTree Int a = ...

是不是真的有可能。最終類型（由KDTree構造）取決於Int的值，它需要一個稱爲依賴類型的功能。像Agda和Epigram這樣的語言支持這一點，但不支持Haskell。

來源

2011-09-01 09:21:59

謝謝你。 Vec似乎是我學習如何做到這一點的最簡單可能的例子。 –

是的，Vec可能是最簡單的，然後Dimensional。 llvm和ForSyDe更復雜，雖然我認爲他們基本上只是實現與Vec相同的功能。 –

在Haskell中使用整數參數化類型

回答

相關問題