作为我的第一门编程语言,我决定学习Haskell.我是一个分析哲学专业,Haskell允许我快速而正确地创建感兴趣的程序,例如,用于自然语言解析的传感器,定理证明器和解释器.虽然我只编写了两个半月的编程,但我发现Haskell的语义和语法比传统的命令式语言更容易学习,并且对其大多数构造感到舒适(现在).
然而,Haskell中的编程就像巫术,我想拓宽我对编程的了解.我想选择一种新的编程语言来学习,但我没有足够的时间来学习任意语言,删除它并重复.所以我想我会在这里提出问题,以及关于我正在寻找的语言类型的几个规定.有些是主观的,有些是为了缓解从Haskell的过渡.
称重答案:当然,这些只是笔记.我只想回复所有给出良好反应的人.你一直非常乐于助人.
1)一些回答表明强调递归的强大的静态类型语言意味着另一种功能语言.虽然我想继续与Haskell合作,但是camccann和larsmans正确地指出另一种这样的语言会"过度缓解过渡".这些评论非常有用,因为我不打算在Caml中编写Haskell!在证明助理中,Coq和Agda看起来都很有趣.特别是,Coq将为建构逻辑和形式类型理论提供可靠的介绍.我花了一点时间使用一阶谓词和模态逻辑(Mendellsohn,Enderton,一些Hinman),所以我可能会对Coq有很多乐趣.
2)其他人非常青睐Lisp(Common Lisp,Scheme和Clojure).从我收集的内容来看,Common Lisp和Scheme都有很好的介绍性材料(On Lisp和The Reasoned Schemer,SICP).SICP中的材料使我倾向于Scheme.特别是,通过SICP的Scheme将涵盖不同的评估策略,懒惰的实现,以及关注诸如延续,解释器,符号计算等主题的机会.最后,正如其他人所指出的那样,Lisp对代码/数据的处理将是全新的.因此,我倾向于选择(2),一个Lisp.
3)第三,Prolog.Prolog有很多有趣的材料,它的主要领域正是我感兴趣的.它具有简单的语法并且易于阅读.我现在无法评论更多,但在阅读了Prolog的概述并浏览了一些介绍材料之后,它排名为(2).似乎Prolog的回溯总是被黑客入侵Haskell!
4)在主流语言中,Python看起来最有趣.蒂姆耶茨使这些语言听起来非常吸引人.显然,Python经常被教给第一年的CS专业; 所以它要么在概念上丰富,要么易于学习.我需要做更多的研究.
谢谢大家的推荐!它看起来像Lisp(Scheme,Clojure),Prolog或像Coq或Agda这样的证明助手是推荐的主要语言.
假设我有一个状态monad,例如:
data Registers = Reg {...}
data ST = ST {registers :: Registers,
memory :: Array Int Int}
newtype Op a = Op {runOp :: ST -> (ST, a)}
instance Monad Op where
return a = Op $ \st -> (st, a)
(>>=) stf f = Op $ \st -> let (st1, a1) = runOp stf st
(st2, a2) = runOp (f a1) st1
in (st2, a2)
功能如
getState :: (ST -> a) -> Op a
getState g = Op …我有一个数据类型
data N a = N a [N a]
玫瑰树和应用实例
instance Applicative N where
pure a = N a (repeat (pure a))
(N f xs) <*> (N a ys) = N (f a) (zipWith (<*>) xs ys)
并需要证明适用法律.然而,纯粹创造无限深,无限分枝的树木.因此,例如,在证明同态定律
pure f <*> pure a = pure (f a)
我认为这证明了平等
zipWith (<*>) (repeat (pure f)) (repeat (pure a)) = repeat (pure (f a))
通过近似(或采取)引理将起作用.然而,我的尝试导致归纳步骤中的"恶性循环".特别是减少
approx (n + 1) (zipWith (<*>) (repeat (pure f)) (repeat (pure a))
给
(pure f <*> …我已经习惯了Haskell的高阶函数.通常我可以使用map,fold和scan等函数替换显式的递归模式.但是,我经常遇到以下递归模式,我不明白如何使用高阶函数表达:
f (x:[]) = k x
f (x:xs) = g x (f xs)
例如,假设我代表分析表.然后我创建一个数据类型,如:
data Tableau = N Expr | S Expr (Tableau) | B Expr (Tableau) (Tableau)
如果我想将Exprs 列表转换为tableau结构,我想要一个函数部分可能类似于:
f (x:[]) = N x
f (x:xs) = S x (f xs)
现在,我看到三个选项:(1)创建一个函数,在给定一个画面和一个列表的情况下,决定画面中的下一个分支是否应该是S或N(或者B,我们将忽略该情况); (2)使用高阶函数来封装递归模式f; (3)使用类似的功能f.
最好的选择是什么？
我在Coq中从模块导入定义时遇到问题.我是Coq的新手,但无法使用该语言的参考手册或在线教程解决问题.我有一个模块定义了有限集的签名和公理,我打算在另一个模块中实现.还有更多,但它看起来像这样(作为参考,我正在密切关注Filliatre关于有限自动机的论文):
Module FinSet.
...
Parameter fset : Set -> Set.
Parameter member : forall A : Set, A -> finset A -> Prop.
Parameter emptyset : forall A : Set, fset A.
Parameter union : forall A : Set, fset A -> fset A -> fset A.
...
Axiom axiom_emptyset :
forall A : Set, forall a : A, ~ (member a (emptyset A)).
Axiom axiom_union :
forall A : Set, forall a b : fset A, forall x : …使用类型族,我们可以定义一个类型的函数fold和该类型的底层代数,表示为函数和常量值的n元组.这允许定义在Foldable类型类中定义的通用foldr函数:
import Data.Set (Set)
import Data.Map (Map)
import qualified Data.Set as S
import qualified Data.Map as M
class Foldable m where
type Algebra m b :: *
fold :: Algebra m b -> m -> b
instance (Ord a) => Foldable (Set a) where
type Algebra (Set a) b = (b, a -> b -> b)
fold = uncurry $ flip S.fold
instance (Ord k) => Foldable (Map k a) where
type …在阅读(并略读)Wadler关于monad的论文之后,我决定更仔细地研究这篇论文,为他描述的每个monad定义函子和应用实例.使用类型同义词
type M a = State -> (a, State)
type State = Int
Wadler用于定义状态monad,我有以下(使用相关的名称,所以我可以稍后用newtype声明定义它们).
fmap' :: (a -> b) -> M a -> M b
fmap' f m = \st -> let (a, s) = m st in (f a, s)
pure' :: a -> M a
pure' a = \st -> (a, st)
(<@>) :: M (a -> b) -> M a -> M b
sf <@> sv = \st -> let (f, st1) = sf st
(a, st2) …我可以使用类型类型在Coq中天真地构建代数结构的层次结构.我在查找Coq语法和类型类语义方面遇到了一些麻烦.但是,我相信以下是半群,幺半群和交换幺半群的正确实现:
Class Semigroup {A : Type} (op : A -> A -> A) : Type := {
op_associative : forall x y z : A, op x (op y z) = op (op x y) z
}.
Class Monoid `(M : Semigroup) (id : A) : Type := {
id_ident_left : forall x : A, op id x = x;
id_ident_right : forall x : A, op x id = x
}.
Class AbelianMonoid `(M : Monoid) : Type := …我有一个表示谓词逻辑公式的标准数据类型.表示析出的自然演绎消除规则的函数可能如下所示:
d_el p q =
if p =: (Dis r s) && q =: (Neg r) then Just s else
if q =: (Dis r s) && p =: (Neg r) then Just s else
Nothing where r,s free
x =: y = (x =:= y) == success
在统一失败时,该函数不返回Nothing,而是返回以下解决方案PACKS:
logic> d_el (Dis Bot Top) (Not Bot)
Result: Just Top
More Solutions? [Y(es)/n(o)/a(ll)] n
logic> d_el (Dis Bot Top) (Not Top)
No more solutions.
我错过了什么,为什么在统一失败时不el评价Nothing？
在没有实现嵌入式逻辑编程语言的情况下,是否有可扩展,有效的方法在Haskell中编写存在语句？通常,当我实现算法时,我想表达存在量化的一阶语句,如
?x.?y.x,y ? xs ? x ? y ? p x y
哪里?在列表上重载.如果我赶时间,我可能会写出看起来很像的明显代码
find p [] = False
find p (x:xs) = any (\y -> x /= y && (p x y || p y x)) xs || find p xs
要么
find p xs = or [ x /= y && (p x y || p y x) | x <- xs, y <- xs]
但是这种方法并不能很好地概括为返回多个arities的值或谓词或函数的查询.例如,即使是一个简单的陈述
?x.?y.x,y,z ? xs ? x ? y ? z ? f …