文件名称：coq-io:使用免费monad在Coq中建模IO
文件大小：8KB
文件格式：ZIP
更新时间：2024-05-18 12:04:58
monads coq Coq
在Coq中为IO建模的免费monad 一个小示例，说明如何使用免费的monad对Coq中的原始操作建模各种IO，包括如何提取和运行以这种方式编写的代码。 在，我们需要对有权访问磁盘的程序进行建模。 我们将代码编写在浅层嵌入程序的程序中，该程序带有用于读写磁盘的基元。 这种浅层嵌入是所需的原始磁盘操作上的免费monad。 我们给单子程序一个语义，作为从一种状态到另一种状态的过渡系统。 程序是monad中的值，type参数给出已完成程序的返回值的类型。 状态由基元操纵，基元的行为也在语义中指定。 此处的代码具有类似的模型，但是是以更通用的方式编写的，并且试图仅公开理解概念并运行简单示例所需的细节。 它的工作方式几乎与FSCQ磁盘程序相同，但是用简单的单字节API访问单个输入文件来表述。 概述 Coq模型有一个非常通用的定义prog ，它带有一个参数Op : Type -> Type给出了
【文件预览】：
coq-io-master
----.gitignore(36B)
----Makefile(126B)
----LICENSE(1KB)
----word-count()
--------.gitignore(14B)
--------app()
--------Setup.hs(46B)
--------src()
--------word-count.cabal(836B)
--------README(125B)
--------stack.yaml(324B)
----README.md(3KB)
----Prog.v(6KB)