小编Dag*_*Dag的帖子

证明

在这篇博客文章中,Tekmo指出我们可以证明ExitSuccess退出是因为(我认为)它就像Const构造函数的仿函数(它不具有x这样的fmap行为const).

通过操作包,Tekmo的TeletypeF翻译可能是这样的:

data TeletypeI a where
    PutStrLn :: String -> TeletypeI ()
    GetLine :: TeletypeI String
    ExitSuccess :: TeletypeI ()

我已经读过,操作与一个免费的monad是同构的,但我们可以在这里证明ExitSuccess退出吗？在我看来,它遇到了完全相同的问题exitSuccess :: IO (),特别是如果我们要为它编写一个解释器,我们需要写它就好像它没有退出:

eval (ExitSuccess :>>= _) = exitSuccess

与不涉及任何模式通配符的免费monad版本相比:

run (Free ExitSuccess) = exitSuccess

怠惰

在操作Monad教程中, apfelmus提到了一个缺点:

状态monad表示为s - >(a,s)可以应对一些无限的程序,如

evalState (sequence . repeat . state $ \s -> (s,s+1)) 0

Run Code Online (Sandbox Code Playgroud)

而指令列表方法没有希望处理它,因为只有最后一个Return指令才能返回值.

对于免费的monad也是如此吗？

令我感到震惊的是,每个monad理解都以a结尾return.这不能有效地使它们与应用程序编程同构吗？为什么我们有一个Monad约束的monad理解而不是一个约束的应用理解Applicative？

对于Applicative来说,这种类似于符号的符号类似于monad理解.

我正在尝试为强类型文件路径创建一个通用的自由类别（路径）和文件系统实例。我希望新的TypeInType扩展能够使这种更通用的路径类型成为可能，我在 2013 年的早期工作似乎需要将文件系统部分绑定到类别部分，但我遇到了一个问题，我似乎不这样做即使它被:kindGHCI接受，也可以将数据族实例提升到类型级别。

我可能会遗漏一些明显的东西；我已经离开 Haskell 和编程有一段时间了，即使那时我也不是高级类型级编程的专家。

我想要在 GHC 8 中实现的目标可能吗？

代码

{-# LANGUAGE TypeInType, TypeFamilies, GADTs #-}\n\nimport Data.Kind\n\ndata family Vertex g\n\ndata family Edge g (a :: Vertex g) (b :: Vertex g)\n\ndata Path g (a :: Vertex g) (b :: Vertex g) where\n    Nil :: Path g a a\n    Cons :: Edge g a b -> Path g b c -> Path g a c\n\ndata FileSystem\n\ndata instance Vertex FileSystem = …