1樓：祖與佔
看到無限巢狀型別 正經 Haskeller 的膝跳反射應該是 free monad, 然後開啟 ekmett 的 free: Monads for free, (經過大佬劇透)發現非常合適 Control.Monad.
Trans.Iter, 然後證明 IterT a 和 Parens a 同構:
後面怎麼實現留作習題, 因為我也不會.
P.S. 上面都是複製大佬的
2樓：ayanamists
當你寫出
data Paren n where
PEmpty :: Paren Z
PLeft :: Paren n -> Paren (S n)
PRight :: Paren (S n) -> Paren n
這個東西的時候，你應該意識到了，這個問題有兩種方法可以實現：
如果n是乙個『型別』，那麼Paren相當於乙個高階型別，是從把型別對映到型別的函式
如果n是乙個『資料』，那麼Paren相當於乙個把資料對映到型別的函式，這就是dependent type.
那這個用有Dependent type的語言好實現嗎？比如Coq？
Inductive
Paren
:nat
->Type:=|
PEmpty
:Paren0|
PLeft(n
:nat)(
p:Parenn)
:Paren(S
n)|PRight(n
:nat)(
p:Paren(S
n)):Parenn.
InductiveP:=
|Left
|Right
.Fixpoint
makeParen:(
n:nat)(p
:(Parenn))
->listP:=
matchn,
pwith
雖然可以定義乙個接受Paren n的函式， 但要命的是，Coq的match，匹配的是constructor，不是型別。
不過，Coq裡面的match不是沒有一點匹配型別的能力，它能用類似於這樣的語法匹配型別match ... as ... in ...
return ... with ...，但是匹配型別做啥呢？
它做的實際上是根據不同的型別返回不同的型別， 而不是根據不同的型別返回不同的值。
所以，如果你想根據不同的型別返回不同的值，我個人傾向於不太行。
3樓：
不是很懂你們這種寫型別寫魔怔的，當無型別寫不好麼，想證什麼就 informal 地寫好了。把 type erase 以後要怎麼執行想好了，不然就是指望有不存在的魔法至極的 staging 了。
data
Paren
=PEmpty
|PLeft
Paren
|PRight
Paren
instance
Show
Paren
where
show
PEmpty=""
show
(PLeftp)
='('
:show
pshow
(PRightp)
=')'
:show
ppush
=PLeft
pop=
PRight
fin::
Paren
->String
-- Paren Z -> String
finp
=reverse
(showp)
size
::Paren
->Int-- Paren x ->
size
PEmpty=0
size
(PLeftp)
=succ
(sizep)
size
(PRightp)
=pred
(sizep)
pair
::Paren
->Paren
-- Paren n -> Paren Zpairp=
aux(
sizep)
pwhere
aux0p=
pauxnp
=aux
(predn)
(popp)
makeParen
::Int
->Paren
->String
-- Int -> Paren n -> StringmakeParen0p
=fin
(pairp)
makeParennp
|sizep==
0=makeParen(n
-1)(
pushp)
|otherwise
=makeParen(n
-1)(
pushp)
++makeParenn(
popp
)main
=putStrLn
(makeParen
3PEmpty
)拿 Haskell 當 proof assistant 用可還行。就算給我 Liquid 我也懶得寫 size 的性質證明
Haskell 中如何描述 product 作為 的 category？
張智浩 首先這個問題表述確實不大清楚，至少不是嚴格的數學語言 或者說不大精確 我把問題重新表述如下 此處快速回憶範疇的定義，略 或可參見維基百科 性質 對任意三個物件 復合對映 是同構。不精確的問題 若乙個範疇滿足性質 我們能對它說些什麼嗎？從某些 可能沒用的 經驗來看，這種問題一般就取特殊值就完了...
如何理解Haskell中的函式呼叫
並不是你想的語法糖，按照你的思路，只返回的函式咋辦？事實是這是一種叫柯里化的東西，用必應會谷歌自行查詢 Currying Function 事實上，對於Haskell 很多地方與一般的面相過程與物件的語言是不一樣的。 UWRF 對於 a b 是函式嗎？a 和 b 是什麼不重要，但 a 和 b 的型別...
如何解釋 Haskell 中的單子（Monad）？
陳斌 自函子的Monoidal範疇上的乙個么半群.么半群是指.大概意思.原群 這班裡全是小學生,希望揍他們任意有限次後還是小學生.這在拓撲概念裡可能要求更過分,揍任意無數次必須還是小學生.半群 在原群基礎上,小學生排好隊了之後,我希望先揍任意相鄰兩個,結果都一樣.么半群 在半群基礎上,希望這群小學生...