如何有效地使用leksah haskell IDE？首先,我非常感谢leksah人员所做的所有工作.这太棒了!
但是,我在leksah工作有困难.
mymain :: IO ()
mymain = do
myData <- getMyData
...
...
如何在do-expression中显示某些变量的类型,比如myData？当我右键单击它然后转到键入时,错误消息得到<interactive>:1:1: Not in scope: 'myData'.在我用leksah中的ghci执行某些操作后,build(CtrlB)不再编译我的项目,但突然做了其他事情.
我怎样才能有效地使用leksah,特别是关于leksah中的ghci(比如显示一种不是顶层而是嵌套的东西)？你会建议的五大要点是什么？
什么是函数的有效名称？
例子
-- works
let µ x = x * x
let ö x = x * x
-- doesn't work
let € x = x * x
let § x = x * x
我不确定,但我的预感是Haskell不允许使用Unicode函数名称,是吗？(如http://www.cse.chalmers.se/~nad/listings/lib-0.4/Data.List.html中的 Unicode )
在R中有类似函数组合的东西吗？
我认为在haskell中它有点像"(.)"而在agda中它是环形运算符.
另外,我在R中找到关于高级函数式编程的小信息.我发现函数"Reduce","Map","Filter"......还有更多吗？有什么指针吗？
我想解析一个String描述命题公式,然后用SAT求解器找到命题公式的所有模型.
现在我可以用hatt包解析一个命题公式; 看testParse下面的功能.
我也可以用SBV库运行SAT求解器调用; 看testParse下面的功能.
问题:
如何在运行时生成Predicate类似于myPredicateSBV库中的类型值,该值表示我刚从String中解析的命题公式？我只知道如何手动键入forSome_ $ \x y z -> ...表达式,而不知道如何将转换器函数从Expr值写入类型的值Predicate.
-- cabal install sbv hatt
import Data.Logic.Propositional
import Data.SBV
-- Random test formula:
-- (x or ~z) and (y or ~z)
-- graphical depiction, see: https://www.wolframalpha.com/input/?i=%28x+or+~z%29+and+%28y+or+~z%29
testParse = parseExpr "test source" "((X | ~Z) & (Y | ~Z))"
myPredicate :: Predicate
myPredicate = forSome_ $ \x y z -> …我有兴趣为在Haskell中实现命令式语言的项目使用更有效的指针.已有一个库:Struct.有一篇博客文章和简要文档.
问题是链接树只有一个非常复杂的例子.对于像我这样每天不使用Haskell的人来说,与文档代码,模板haskell等进行战斗是相当费力的.
我需要一个简单的例子来开始,沿着表达这两种数据类型的方式:
import Data.IORef
data DLL a = DLL a (Maybe (IORef (DLL a))) (Maybe (IORef (DLL a)))
data DLLINT = DLLINT Int (Maybe (IORef DLLINT)) (Maybe (IORef DLLINT))
对于熟练使用Haskell/GHC的人来说,这应该只是一些简单的界限.
如何使用Struct库表达上述数据类型之一？
我试图解析Agda中的嵌套列表.我在谷歌搜索,我发现最接近的是在Haskell中解析,但通常使用像"parsec"这样的库,这些库在Agda中不可用.
所以我想"((1,2,3),(4,5,6))"用结果类型解析(List (List Nat)).
并且应该支持进一步的嵌套列表(直到深度5),例如,深度3将是(List (List (List Nat))).
我的代码非常冗长和繁琐,它只适用于(List (List Nat))但不适用于其他嵌套列表.我自己没有取得任何进展.
如果有帮助,我想splitBy从我的一篇旧帖子的第一个答案中重复使用.
NesList : ? ? Set
NesList 0 = ? -- this case is easy
NesList 1 = List ? -- this case is easy
NesList 2 = List (List ?)
NesList 3 = List (List (List ?))
NesList 4 = List (List (List (List ?)))
NesList 5 = List (List (List (List (List ?)))) -- I …这是一个棘手的问题.
但是+1在嵌套列表上映射函数(在本例中)的标准方法是什么？
map (\x -> map (+1) x) [[1,2,3],[4,5,6]]
我在我的代码中使用了上述方法,但有什么好办法呢？有类似的东西mapNested (+1) [[1,2,3],[4,5,6]]吗？我使用谷歌和hoogle但得到了太多的通用结果.
在ICFP 2012上,Conor McBride发表了主题演讲,主题为"Agda-curious？".
它具有小型堆栈机器实现.
视频在youtube上:http://www.youtube.com/watch？v = XGyJ519RY6Y
代码也在线:http: //personal.cis.strath.ac.uk/conor.mcbride/ICFP12Code.tgz
我想知道run第5部分的功能(如果您下载了代码,则为"Part5Done.agda").在run解释函数之前,谈话停止.
data Inst : Rel Sg SC Stk where
PUSH : {t : Ty} (v : El t) -> forall {ts vs} ->
Inst (ts & vs) ((t , ts) & (E v , vs))
ADD : {x y : Nat}{ts : SC}{vs : Stk ts} ->
Inst ((nat , nat , ts) & (E y , E x , vs))
((nat …通常我有问题sledgehammer找到证据,但是当我插入它时,它不会终止.我猜sledgehammer是Isabelle最重要的部分之一,但如果证据失败则会变得很烦人.
在Sledgehammer教程中,有一个小章节"为什么Metis无法重建证明？".
它列出:
isar_proofs选项以获得逐步的Isar证明,其中每个步骤都是正确的metis.由于步骤相当小,
metis因此更有可能重播它们.smt证明方法而不是metis.它通常更强大,但您需要使用Z3重放证明,信任SMT求解器或使用证书.blast或者auto证明方法,通过传递必要的事实unfolding,using,intro:,elim:,dest:,或simp:适当.问题是第一个选项使证明更加冗长,并且还涉及手动干预.第二种选择很少有效.
那么第三种选择呢？我可以使用任何易于遵循的启发式方法吗？
unfolding和之间有什么区别using？也有关于如何使用的最佳做法intro:,elim:以及dest:从失败的metis证明吗？
部分例子
proof-
have "(det (?lm)) = (det (transpose ?lm))" by (smt det_transpose)
then have "(det (?lm)) = [...][not shown]"
unfolding det_transpose transpose_mat_factor_col by auto
then show ?thesis [...][not …我明天参加一个大型的编程竞赛,在那里我使用R.
时间是主要因素(7个编码问题仅2小时).问题与数学有关.
我定义一个函数时,我想写"f"而不是"function".这可以完成,我有代码这样做,但我失去了它,无法找到它.
我在哪里找到sin()函数用于度输入,而不是弧度？
(可选)是否有任何特定于算法的任务视图或库.
编程竞赛的任何提示？
我为比赛准备了以下备忘单:http: //pastebin.com/h5xDLhvg
========编辑:==========
所以我终于有时间写下我的经验教训了.
编程比赛非常有趣,但遗憾的是我得分不是很高.我排在前50%,但我的目标是进入前25%.
主要问题是编程时间很短,总共只有2个小时.但我必须阅读问题描述,而且我还需要一些时间将结果粘贴到网络表单等等,所以它更像是90分钟的编程.
希望12月的下一场比赛将延长时间,比如3-4个小时.组织者说也许会是这样的.
此外,比赛没有互联网访问,我的移动接待并没有真正起作用.
对我来说,主要的教训是你必须使用你日常使用的语言才能获得真正的机会.特别是,如果只有大约90分钟的时间来编程.由于我在日常工作中使用的是haskell而不是R,我认为R不是最好的选择.在比赛期间,我混淆了haskell和R函数定义,并且我编写了太多小错误来编程足够快.
比赛的好处在于,大约80名参赛者共获得了大约2万美元的奖金.因此,前25%的参与者每人获得500至1500美元.此外,我认为前15%的人能够立即获得一家赞助商IT公司的工作.
所以这是一个双赢的局面.这很有趣,而且你可以获得奖金.此外,IT公司非常高兴,因为他们可以访问顶级程序员.
我利用这个机会与IT决策者交流.其中一个来自一家大银行.我大胆地建议他们考虑转换到Scala进行开发(来自Java的转换).还要考虑使用R和Haskell.很有趣,他们甚至说他们已经看过Scala了!
值得注意的是,我最好的朋友之一在比赛中表现非常出色.他只有19岁,但他在前20%中排名第一,获得了500美元的奖金.他打败了我和我的6所大学,他们都拥有可敬的计算机科学学位.我的朋友程序更像是黑客风格,但他的速度非常快.
使用前10名的人:1)Java 2)C#和3)C++(前10名中没有其他编程语言!).我认为唯一合理得分的编程语言是Ruby.
对于下一次比赛,选择的编程语言可能是haskell.出于一个原因,为haskell找到2个队友比为R编程更容易.最多可以有3人组成一个团队.
我的理想情况是一个非常轻量级的框架,我可以同时使用多种编程语言进行比赛.这样,主代码可以用haskell编写(所有队友都可以编程).一些特定的函数可以用R,Mathematica,甚至其他编程语言(如python/sage)编程.
这听起来有点矫枉过正.但我认为这将是非常有用的.就像一个函数,它有一个矩阵作为参数并返回一个矩阵.然后这个框架工作从R代码自动生成RESTful服务,所以我可以从任何编程语言调用R函数.矩阵只是作为JSON数据(或其他一些序列化)传递.好的,但这不是主题......
最后一些经验教训作为子弹列表:
非常感谢'Iterator'的帮助!