我是依赖类型的新手,我对这两者之间的区别感到困惑.看来人们通常说一个类型是由其他类型的参数,并通过一定的价值索引.但是,依赖类型语言中的类型和术语之间没有区别吗？参数和指数之间的区别是否基本？你能告诉我在编程和定理证明中它们的含义不同的例子吗？
功能语言中的GADT是否等同于传统的OOP +泛型,或者存在GADT容易强制执行但使用Java或C#难以实现或无法实现的正确性约束的情况？
例如,这个"井型解释器"Haskell程序:
data Expr a where
N :: Int -> Expr Int
Suc :: Expr Int -> Expr Int
IsZero :: Expr Int -> Expr Bool
Or :: Expr Bool -> Expr Bool -> Expr Bool
eval :: Expr a -> a
eval (N n) = n
eval (Suc e) = 1 + eval e
eval (IsZero e) = 0 == eval e
eval (Or a b) = eval a || eval b
可以使用泛型和每个子类的适当实现在Java中等效编写,但更详细:
interface …如何使用Agda的输入法在非Agda模式下输入unicode字符？我尝试时看不到它的名字set-input-method.我想使用Agda的输入法而不是TeX因为我想要的字符无法输入TeX.
或者,可能另一个问题是"如何在现有TeX输入法中添加更多快捷方式来输入unicode字符？"
非常感谢你
当Emacs中弹出自动完成菜单时,除了向上和向下箭头之外,我还可以用什么键在菜单中上下导航？我尝试过C-n,C-p但这会使菜单消失并在文本区域上下移动光标.
values和list或cons在Racket或Scheme 之间有什么区别？什么时候使用一个比另一个好？例如,如果quotient/remainder返回(cons _ _)而不是(values _ _)？
我是F#的新手,并编写了一些简单的算法来习惯这种语言,这需要argMax.标准库是否具有搜索最大化函数的列表元素的功能？也就是说,如果现有函数的行为与此类似:
let argMax f xs =
let rec go a fa zs =
match zs with
| [] -> a
| z :: zs' ->
let fz = f z
if fz > fa
then go z fz zs'
else go a fa zs'
match xs with
| [] -> invalidArg "xs" "empty"
| x :: xs' -> go x (f x) xs'
我想Emacs使用Qt和Common Lisp作为业余爱好项目实现另一个,仅供我自己学习.但我不确定是否存在"Emacs的官方规范"这样的事情,以便我可以遵循以确保与其他实现的最大兼容性,比如说GNU Emacs？
我开始学习伊莎贝尔,并想尝试在伊莎贝尔中定义一个幺半群,但不知道如何.
在Coq中,我会做这样的事情:
Inductive monoid (? : Type) (op: ? -> ? -> ?) (i: ?): Prop :=
| axioms: (forall (e: ?), op e i = e) ->
(forall (e: ?), op i e = e) ->
monoid ? op i.
我不知道如何在伊莎贝尔做同样的事情.从概念上讲,我想到了这样的事情:
inductive 'a monoid "('a ? 'a ? 'a) ? 'a ? bool" for f i where
axioms: "?f e i = e; f i e = e? ? monoid f i"
但是,这在Isabelle中无效.
如何在Isabelle中使用类型参数定义归纳谓词？
我在OCaml FFI上学习了本教程并Ctypes通过OPAM 安装:
opam install ctypes
但是,OCaml找不到该模块:
open Ctypes
(* ... *)
我收到错误:
Unbound module Ctypes
看起来我需要让OCaml知道我的Ctypes安装位置在哪里？我是否需要更新一些路径变量以让OCaml查找通过OPAM安装的库？
这是Ubuntu 15.04,OCaml 4.01.0,OPAM 1.2.0.