更新时间:2023-11-20 23:01:52
标语关注类型!" 在这里为我们全职工作.
The slogan, "Follow the types!", works for us here, fulltime.
从您的代码中进行一些重命名,以便于理解,
From your code, with some renaming for easier comprehension,
{-# LANGUAGE RankNTypes #-}
data ListF a r = Nil | Cons a r deriving (Show)
newtype List a = Mu {runMu :: forall r. (ListF a r -> r) -> r}
这样我们就可以拥有
fromList :: [a] -> List a
fromList (x:xs) = Mu $ \g -> g -- g :: ListF a r -> r
(Cons x $ -- just make all types fit
runMu (fromList xs) g)
fromList [] = Mu $ \g -> g Nil
{- or, equationally,
runMu (fromList (x:xs)) g = g (Cons x $ runMu (fromList xs) g)
runMu (fromList []) g = g Nil
such that (thanks, @dfeuer!)
runMu (fromList [1,2,3]) g = g (Cons 1 (g (Cons 2 (g (Cons 3 (g Nil))))))
-}
我们想要
instance (Show a) => Show (List a) where
-- show :: List a -> String
show (Mu f) = "(" ++ f showListF ++ ")" -- again, just make the types fit
...我们必须产生一个字符串;我们只能致电 f
;它的论点是什么?根据其类型
... we must produce a string; we can only call f
; what could be its argument? According to its type,
where
showListF :: Show a => ListF a String -> String -- so that, f showListF :: String !
showListF Nil = ...
showListF (Cons x s) = ...
在这里似乎没有其他方法可以连接导线.
There doesn't seen to be any other way to connect the wires here.
以此,print $ fromList [1..5]
打印(1 2 3 4 5 )
.
实际上,这是 chi 的 g
用于代数"(谢谢@chi!),f
(在Mu f
中)用于折叠".现在,这种类型的含义变得更加清晰:给定代数"(归约函数),Mu f
值将在该折叠函数"所表示的固有列表"的折叠中使用它.它在折叠的 each 步骤中使用单步归约语义表示列表的折叠.
edit: g
is for "algebra" (thanks, @chi!) and f
(in Mu f
) is for "folding". Now the meaning of this type becomes clearer: given an "algebra" (a reduction function), a Mu f
value will use it in the folding of its "inherent list" represented by this "folding function". It represents the folding of a list with one-step reduction semantics, using it on each step of the folding.