技术控

    今日:109| 主题:49179
收藏本版 (1)
最新软件应用技术尽在掌握

[其他] Djinn, a theorem prover in Haskell, for Haskell (2005)

[复制链接]
迷恋你的眼 发表于 2016-10-13 01:21:26
63 3

立即注册CoLaBug.com会员,免费获得投稿人的专业资料,享用更多功能,玩转个人品牌!

您需要 登录 才可以下载或查看,没有帐号?立即注册

x
Lennart Augustsson    announced Djinnon the Haskell mailing list recently.  
  He included this demonstration:
        I've written a small program that takes a (Haskell) type
      and gives you back a function of that type if one exists.
      It's kind of fun, so I thought I'd share it.
        It's probably best explained with a sample session.
   
  1. calvin% djinn
  2.    Welcome to Djinn version 2005-12-11.
  3.    Type :h to get help.
  4. # Djinn is interactive if not given any arguments.
  5. # Let's see if it can find the identity function.
  6.    Djinn> f ? a->a
  7.    f :: a -> a
  8.    f x1 = x1
  9. # Yes, that was easy.  Let's try some tuple munging.
  10.    Djinn> sel ? ((a,b),(c,d)) -> (b,c)
  11.    sel :: ((a, b), (c, d)) -> (b, c)
  12.    sel ((_, v5), (v6, _)) = (v5, v6)
  13. # We can ask for the impossible, but then we get what we
  14. # deserve.
  15.    Djinn> cast ? a->b
  16.    -- cast cannot be realized.
  17. # OK, let's be bold and try some functions that are tricky to write:
  18. # return, bind, and callCC in the continuation monad
  19.    Djinn> type C a = (a -> r) -> r
  20.    Djinn> returnC ? a -> C a
  21.    returnC :: a -> C a
  22.    returnC x1 x2 = x2 x1
  23.    Djinn> bindC ? C a -> (a -> C b) -> C b
  24.    bindC :: C a -> (a -> C b) -> C b
  25.    bindC x1 x2 x3 = x1 (\ c15 -> x2 c15 (\ c17 -> x3 c17))
  26.    Djinn> callCC ? ((a -> C b) -> C a) -> C a
  27.    callCC :: ((a -> C b) -> C a) -> C a
  28.    callCC x1 x2 = x1 (\ c15 _ -> x2 c15) (\ c11 -> x2 c11)
  29. # Well, poor Djinn has a sweaty brow after deducing the code
  30. # for callCC so we had better quit.
  31.    Djinn> :q
  32.    Bye.
复制代码
     To play with Djinn do a
      darcs get http://darcs.augustsson.net/Darcs/Djinn
      or get
              http://darcs.augustsson.net/Darcs/Djinn/Djinn.tar.gz      
      Then just type make. (You need a Haskell 98 implementation and
      some libraries.) And then start djinn.
          For the curious, Djinn uses a decision procedure for intuitionistic
      propositional calculus due to Roy Dyckhoff. It's a variation of
      Gentzen's LJ system. This means that (in theory) Djinn will always
      find a function if one exists, and if one doesn't exist Djinn will
      terminate telling you so.
        This is the very first version, so expect bugs. :)
    Don Stewart wrote a lambdabot plugin for Djinn a few hours later.
  1. 15:39:01  @djinn a -> b -> a
  2. 15:39:02  x :: a -> b -> a
  3. 15:39:02  x x1 _ = x1
  4. 15:39:11  @djinn (a -> b -> c) -> ((a,b) -> c)
  5. 15:39:11  x :: (a -> b -> c) -> (a, b) -> c
  6. 15:39:11  x x1 (v3, v4) = x1 v3 v4
  7. 15:39:27  @djinn (a -> b) -> (c -> b) -> Either a c -> b
  8. 15:39:27  x :: (a -> b) -> (c -> b) -> Either a c -> b
  9. 15:39:27  x x1 x2 x3 = case x3 of
  10. 15:39:27       Left l4 -> x1 l4
  11. 15:39:27       Right r5 -> x2 r5
  12. 15:40:06  @djinn a -> [a] -> [a]
  13. 15:40:07  x :: a -> [a] -> [a]
  14. 15:40:07  x _ x2 = x2
  15. 15:40:08  @help djinn
  16. 15:40:09   @djinn
  17. 15:40:09  Generates Haskell code from a type.
复制代码
Djinn has proven to be much fun on #haskell.
友荐云推荐




上一篇:Faster PostgreSQL Counting
下一篇:Meet the team: Martina Janevska – Problem solver who loves a challenge
酷辣虫提示酷辣虫禁止发表任何与中华人民共和国法律有抵触的内容!所有内容由用户发布,并不代表酷辣虫的观点,酷辣虫无法对用户发布内容真实性提供任何的保证,请自行验证并承担风险与后果。如您有版权、违规等问题,请通过"联系我们"或"违规举报"告知我们处理。

mohamode 发表于 2016-10-13 05:31:59
回帖淹没我们,潜水拆散我们
回复 支持 反对

使用道具 举报

yakte7 发表于 2016-10-13 07:29:03
楼主的头像是本人吗?
回复 支持 反对

使用道具 举报

承茗达z 发表于 2016-10-13 10:17:39
心里只有你一个频道,最可恨的是还没有广告。
回复 支持 反对

使用道具 举报

*滑动验证:
您需要登录后才可以回帖 登录 | 立即注册

本版积分规则

我要投稿

推荐阅读

扫码访问 @iTTTTT瑞翔 的微博
回页顶回复上一篇下一篇回列表手机版
手机版/CoLaBug.com ( 粤ICP备05003221号 | 文网文[2010]257号 )|网站地图 酷辣虫

© 2001-2016 Comsenz Inc. Design: Dean. DiscuzFans.

返回顶部 返回列表