迷恋你的眼 发表于 2016-10-13 01:21:26
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.
To play with Djinn do a 复制代码
- calvin% djinn
- Welcome to Djinn version 2005-12-11.
- Type :h to get help.
- # Djinn is interactive if not given any arguments.
- # Let's see if it can find the identity function.
- Djinn> f ? a->a
- f :: a -> a
- f x1 = x1
- # Yes, that was easy. Let's try some tuple munging.
- Djinn> sel ? ((a,b),(c,d)) -> (b,c)
- sel :: ((a, b), (c, d)) -> (b, c)
- sel ((_, v5), (v6, _)) = (v5, v6)
- # We can ask for the impossible, but then we get what we
- # deserve.
- Djinn> cast ? a->b
- -- cast cannot be realized.
- # OK, let's be bold and try some functions that are tricky to write:
- # return, bind, and callCC in the continuation monad
- Djinn> type C a = (a -> r) -> r
- Djinn> returnC ? a -> C a
- returnC :: a -> C a
- returnC x1 x2 = x2 x1
- Djinn> bindC ? C a -> (a -> C b) -> C b
- bindC :: C a -> (a -> C b) -> C b
- bindC x1 x2 x3 = x1 (\ c15 -> x2 c15 (\ c17 -> x3 c17))
- Djinn> callCC ? ((a -> C b) -> C a) -> C a
- callCC :: ((a -> C b) -> C a) -> C a
- callCC x1 x2 = x1 (\ c15 _ -> x2 c15) (\ c11 -> x2 c11)
- # Well, poor Djinn has a sweaty brow after deducing the code
- # for callCC so we had better quit.
- Djinn> :q
darcs get http://darcs.augustsson.net/Darcs/Djinn
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.
Djinn has proven to be much fun on #haskell. 复制代码
- 15:39:01 @djinn a -> b -> a
- 15:39:02 x :: a -> b -> a
- 15:39:02 x x1 _ = x1
- 15:39:11 @djinn (a -> b -> c) -> ((a,b) -> c)
- 15:39:11 x :: (a -> b -> c) -> (a, b) -> c
- 15:39:11 x x1 (v3, v4) = x1 v3 v4
- 15:39:27 @djinn (a -> b) -> (c -> b) -> Either a c -> b
- 15:39:27 x :: (a -> b) -> (c -> b) -> Either a c -> b
- 15:39:27 x x1 x2 x3 = case x3 of
- 15:39:27 Left l4 -> x1 l4
- 15:39:27 Right r5 -> x2 r5
- 15:40:06 @djinn a -> [a] -> [a]
- 15:40:07 x :: a -> [a] -> [a]
- 15:40:07 x _ x2 = x2
- 15:40:08 @help djinn
- 15:40:09 @djinn
- 15:40:09 Generates Haskell code from a type.
上一篇：Faster PostgreSQL Counting
下一篇：Meet the team: Martina Janevska – Problem solver who loves a challenge