> But what I miss when using these proof assistants, and what I have my
> eyes on, is a way to Search ALL The Theorems. In current proof
> assistants, developments are still distributed in "packages" -- and a
> particular development might have already proved a very useful lemma
> that wasn't the
On Mon, Feb 28, 2011 at 7:59 AM, Tom Hawkins wrote:
> I have been wanting to gain a better understanding of interactive
> theorem proving for some time. And I've often wondered: Can theorem
> proving be made into a user-friendly game that could attract mass
> appeal? And if so, could a population
On Mon, 28 Feb 2011 02:58:58 +
Felipe Almeida Lessa wrote:
> On Sun, Feb 27, 2011 at 6:48 AM, by way of bri...@aracnet.com
> wrote:
> > the binding-DSL examples do NOT use the above PRAGMA anywhere in the
> > code.
>
> Probably they have
>
> Extensions: ForeignFunctionInterface
>
> on
That's doing what I want, but I'm not sure why you passed
[(mkModule (stringToPackageId "base") (mkModuleName "Prelude"), Nothing) ]
to setContext. I found that
[mkModule (stringToPackageId "base") (mkModuleName "Prelude")]
matches the type expected by setContext. Perhaps we are using
different a
Daryoush Mehrtash wrote in article
in
gmane.comp.lang.haskell.cafe:
> I see the problem now. But I am confused as to why there are no Bool class
> (like Num, Fractional...) in Haskell. If I had such a class then the
> problem is solved, (by making the "pm a" an instance of it) right? Or are
I see the problem now. But I am confused as to why there are no Bool class
(like Num, Fractional...) in Haskell. If I had such a class then the
problem is solved, (by making the "pm a" an instance of it) right? Or are
there still more issues that I am not seeing?
thanks,
daryoush
On Mon, Feb
Daryoush Mehrtash wrote in haskell-cafe:
> I am confused about this comment:
> > Mostly we preferred (as do the domain experts we target) to write
> > probabilistic models in direct style rather than monadic
>
> In the haskell implementation of the lawn model there are two different
> version of
On 28 February 2011 10:38, Henning Thielemann
wrote:
> Now that almost every syntax can be redirected to custom functions
> (RebindableSyntax, OverloadedStrings), would it make sense to map 'let'
> to 'fix' ?
For the record: are you talking about rewriting:
let f = e in b
into something like:
I'm not particularly familiar with the codebase of either PostgreSQL
or GHC, but I'd be rather surprised that porting GHC's garbage
collector to PostgreSQL would be an easy or worthwhile task. For
example, GHC's garbage collector understands the memory layout that
its data structures use, whic
On 28 February 2011 17:59, Jesper Louis Andersen <
jesper.louis.ander...@gmail.com> wrote:
>
> Many "normal" puzzle games fit into the NP-complete class as well, so
> it would look as if human beings like the challenge of trying to solve
> hard problems. Theorem proving is simply yet another beast
On Mon, Feb 28, 2011 at 17:02, Colin Adams
wrote:
>
> No I haven't. I'm not a mass-market gamer. I'm an ex-hard-core gamer.
>
I think that basically, it is the same psychological stuff that is
going on in the brains of (puzzle) gamers and people who interactively
proves theorems. It is like solvi
> I find this fairly interesting. Once you're finished grappling with the
> logical core, I wouldn't mind helping out with a web interface, time
> permitting. I suspect attracting mass appeal, or getting users at all, is
> helped massively by having a web interface.
Thanks for your interest. Yes,
No I haven't. I'm not a mass-market gamer. I'm an ex-hard-core gamer.
On 28 February 2011 15:53, Daniel Peebles wrote:
> Have you tried it? It's completely addictive (and takes up a big chunk of
> my free time). I'm not sure it'll appeal to everyone, but I wouldn't dismiss
> it off-hand like tha
On 25 February 2011 19:10, Bas van Dijk wrote:
> On 25 February 2011 18:27, sclv wrote:
>>
>>
>> Bas van Dijk-2 wrote:
>>>
>>> I believe the OS threads are created by my levmar library. This
>>> library uses bindings-levmar[4] which is a binding to a C library.
>>> bindings-levmar uses safe FFI c
Have you tried it? It's completely addictive (and takes up a big chunk of my
free time). I'm not sure it'll appeal to everyone, but I wouldn't dismiss it
off-hand like that.
On Mon, Feb 28, 2011 at 10:16 AM, Colin Adams wrote:
> On 28 February 2011 14:59, Tom Hawkins wrote:
>
>> I have been wan
On 28 February 2011 14:59, Tom Hawkins wrote:
> I have been wanting to gain a better understanding of interactive
> theorem proving for some time. And I've often wondered: Can theorem
> proving be made into a user-friendly game that could attract mass
> appeal?
>
No.
I'd wage money on it.
--
I have been wanting to gain a better understanding of interactive
theorem proving for some time. And I've often wondered: Can theorem
proving be made into a user-friendly game that could attract mass
appeal? And if so, could a population of gamers collectively solve
interesting and relevant mathe
Yves Parès wrote:
takeC :: Int -> Compoz a b -> (exists c. Compoz a c)
dropC :: Int -> Compoz a b -> (exists c. Compoz c b)
What does 'exists' means? To create a rank-2 type can't you use:
takeC :: Int -> Compoz a b -> (forall c. Compoz a c)
??
Ah, (exists c. Compoz a c) means "There ex
On Mon, Feb 28, 2011 at 12:41 PM, wren ng thornton wrote:
> On 2/28/11 2:43 AM, Yitzchak Gale wrote:
>>
>> You have written a large software system in Haskell. Wishing to
>> play to Haskell's strength, you have structured your system
>> as a series of composable layers. So you have data types
>>
>
Hi,
On 2011-February-27 Sunday 16:20:06 Edward Amsden wrote:
> Secondly,
>
> I'd like to get to a GHC session that just has, say, Prelude in scope
> so I can use dynCompileExpr with "show" etc, but I cannot figure out
> how to bring it into scope. The closest I got was to get GHC
> complaining th
On 2/28/11 2:43 AM, Yitzchak Gale wrote:
You have written a large software system in Haskell. Wishing to
play to Haskell's strength, you have structured your system
as a series of composable layers. So you have data types
Layer1, Layer2, ...
and functions
layer2 :: Layer1 -> Layer2
layer3 ::
On 2/28/11 6:01 AM, Yves Parès wrote:
takeC :: Int -> Compoz a b -> (exists c. Compoz a c)
dropC :: Int -> Compoz a b -> (exists c. Compoz c b)
What does 'exists' means? To create a rank-2 type can't you use:
takeC :: Int -> Compoz a b -> (forall c. Compoz a c)
??
For any A and T,
On 2/28/11 2:50 AM, Niklas Broberg wrote:
Ah, I suppose that's to do with the trac server itself, that's beyond me.
Moving to café: Does anyone know what's up with trac.haskell.org not sending
out verification emails?
Having just signed up, like a few hours ago, it took a long while for
the v
Hello all,
I've just uploaded the 3.0.0.0 version of Hakyll [1] to Hackage [2].
This is a complete rewrite, and completely backward-incompatible with
previous versions. Sorry for that.
On the other hand, I believe almost all aspects of the library have
improved tremendously. Hakyll now uses a dec
> takeC :: Int -> Compoz a b -> (exists c. Compoz a c)
> dropC :: Int -> Compoz a b -> (exists c. Compoz c b)
What does 'exists' means? To create a rank-2 type can't you use:
takeC :: Int -> Compoz a b -> (forall c. Compoz a c)
??
2011/2/28 Heinrich Apfelmus
> Yitzchak Gale wrote:
>
>> You
Now that almost every syntax can be redirected to custom functions
(RebindableSyntax, OverloadedStrings), would it make sense to map 'let'
to 'fix' ? Would this open a way to implement observable sharing as
needed in EDSLs by a custom 'fix'?
___
Haskell-
Hello,
From what I see here, you can use a well-known technique call descent
recursive parser. The idee is to do exactly what you did but involving
a call to some other function which should do some kind of sub-work.
Actually, you can see the pattern already in the code you provided; for instance
Yitzchak Gale wrote:
You have written a large software system in Haskell. Wishing to
play to Haskell's strength, you have structured your system
as a series of composable layers. So you have data types
Layer1, Layer2, ...
and functions
layer2 :: Layer1 -> Layer2
layer3 :: Layer2 -> Layer3
Hi Thu,
You read my mind. Ok, for the details. Here are my data structur for the
differen tokens (currently not complete):
data GmlToken = IntToken Int
| RealToken Double
| BoolToken Bool
| StringToken String
| FunctionToken TokenSequence
| ArrayToken TokenSequence
29 matches
Mail list logo
