我希望一些Haskell专家可以帮助澄清一些事情.
是否有可能以Nat通常的方式定义(通过Haskell中的 @dorchard Singleton类型)
data S n = Succ n
data Z = Zero
class Nat n
instance Nat Z
instance Nat n => Nat (S n)
(或其一些变体)然后定义一个LessThan关系,使得forall n和m
LessThan Z (S Z)
LessThan n m => LessThan n (S m)
LessThan n m => LessThan (S n) (S m)
然后编写一个类似的函数:
foo :: exists n. (LessThan n m) => Nat m -> Nat n
foo (S n) = n
foo Z = …我正在尝试使用SMTLIB接口为Z3定义集合理论(并集,交集等).不幸的是,我的当前定义为一个简单的查询挂起z3,所以我想我错过了一些简单的选项/标志.
这是固定链接:http: //rise4fun.com/Z3/JomY
(declare-sort Set)
(declare-fun emp () Set)
(declare-fun add (Set Int) Set)
(declare-fun cup (Set Set) Set)
(declare-fun cap (Set Set) Set)
(declare-fun dif (Set Set) Set)
(declare-fun sub (Set Set) Bool)
(declare-fun mem (Int Set) Bool)
(assert (forall ((x Int)) (not (mem x emp))))
(assert (forall ((x Int) (s1 Set) (s2 Set))
(= (mem x (cup s1 s2)) (or (mem x s1) (mem x s2)))))
(assert (forall ((x Int) (s1 Set) (s2 Set))
(= (mem … 我想编写一个简单的函数,迭代文本文件的行.我相信2.8一个人可以这样做:
def lines(filename: String) : Iterator[String] = {
scala.io.Source.fromFile(filename).getLines
}
就是这样,但在2.9上面不起作用,而是我必须这样做:
def lines(filename: String) : Iterator[String] = {
scala.io.Source.fromFile(new File(filename)).getLines()
}
现在,麻烦的是,我想在for理解中组成上面的迭代器:
for ( l1 <- lines("file1.txt"); l2 <- lines("file2.txt") ){
do_stuff(l1, l2)
}
这再次,曾经工作得很好,2.8但导致"太多打开文件"异常被抛出2.9.这是可以理解的 - 理解中的第二个lines
最终打开(而不是关闭)第一个中每行的文件.
在我的情况下,我知道它"file1.txt"很大,我不想把它吸入
内存,但第二个文件很小,所以我可以这样写一个不同的linesEager
:
def linesEager(filename: String): Iterator[String] =
val buf = scala.io.Source.fromFile(new File(filename))
val zs = buf.getLines().toList.toIterator
buf.close()
zs
然后把我的理解变成:
for (l1 <- lines("file1.txt"); l2 <- linesEager("file2.txt")){
do_stuff(l1, …我一直在使用hsenv(非常成功!)来处理通常的cabal依赖问题.
它太棒了,但有一个小故障我无法解决:如何说服(也很棒!)vim-haskellmode使用hsenv设置的环境变量 - 即编译时GHC,cabal数据库等的路径,生成标签等
有谁知道如何解决这个问题？
我正在尝试使用"数据文件"机制,除了相关文件没有复制到share/目录之外,其他工作正常.例如我的.cabal文件看起来像:
name: nano-js
version: 0.1.0.0
data-files: include/prelude.js
但在构建和安装目录之后
.hsenv/cabal/share/nano-js-0.1.0.0
不存在.所以对表单的查询
getDataFileName "include/prelude.js"
产生一个FilePath不存在的
nanojs: /home/rjhala/research/liquid/.hsenv/cabal/share/nano-js-0.1.0.0/include/prelude.js: openFile: does not exist (No such file or directory)
是否需要填写一些额外的关键字share/？
或者这可能是一个问题hsenv？
谢谢!
我已经使用 (ML) z3 绑定一段时间了，API 函数
val mk_distinct : context -> ast array -> ast
多年来一直忠实服务。我现在尝试切换到 SMTLIB2 界面，但我发现该distinct命令是unsupported. 例如，查询：
(declare-fun x () Int)
(declare-fun y () Int)
(distinct x y)
(assert (= x y))
(check-sat)
产生响应：
unsupported
; distinct
sat
在网络演示上。有一些解决方法吗？
谢谢！
兰吉特。
我对以下行为感到困惑：有人可以解释发生了什么吗？
考虑代码：
struct Point {
cx : u32,
}
fn main() {
let mut p1 = Point { cx: 100 };
let p2 = p1;
p1.cx = 5000;
// println!("p1.x = {}", p1.cx); // disallowed as p1.cx is "moved" ... ok
println!("p2.x = {}", p2.cx); // ==> prints 100 (!)
}
具体来说，我感到困惑的是：
p1.cx允许即使举动已经发生，p2.x实际上不是更新后的 5000，而是旧的100.我期待新值，因为没有复制特征（因此移动），所以期待只有一个单元格，其更新值 ( 5000) 应该被打印出来。
但是，我一定错过了一些东西。有小费吗？提前致谢！
假设我有一个包含类型的模块:
module My where
data L a = Nil | Cons a (L a)
模块导出具体的定义My以允许模式匹配等.是否有可能是另一个模块,比如Client以
抽象My的方式导入,L a即L a类型检查器禁止模式匹配值？
有人可以解释解决以下问题的最佳方法,而不是好奇的类型错误.假设我创建了一个元组列表,如下所示:
scala> val ys = List((1,2), (3,4), (5,6))
ys: List[(Int, Int)] = List((1,2), (3,4), (5,6))
现在,如果我想将其映射到List(Int)
scala> ys.map((a: Int, b: Int) => a + b)
<console>:9: error: type mismatch;
found : (Int, Int) => Int
required: ((Int, Int)) => ?
ys.map((a: Int, b: Int) => a + b)
^
有线索吗？我知道我可以使用for comprehension
scala> for ((a, b) <- ys) yield a + b
res1: List[Int] = List(3, 7, 11)
但是在这种情况下破坏理解是错误的.谢谢!