scryer-shen: new implementation in development

[Mark]

Hi all,

I've begun working on an implementation of Shen in Racket which integrates directly with my Scryer Prolog ISO system. Unlike other implementations so far, it's not bootstrapped from KLambda but is implemented directly in its host languages.

If interested, you can follow it here:

https://github.com/mthom/scryer-shen

It may move to another repository host once Github implements 2-factor authentication on February 20.

[dr.mt...@gmail.com]

My congratulations on this significant achievement.

Mark

[Mark]

Thank you Mark. I think I will try to present it at ELS this year. 

Incidentally, one of Scryer Prolog's contributors (the author of the Power of Prolog and the clpz, clpb, and simplex libraries, among many others), Markus Triska, works at the venue hosting the conference.

[dr.mt...@gmail.com]

What's ELS BTW?

Mark

[Mark]

The European Lisp Symposium.

[dr.mt...@gmail.com]

Right; where Shen was announced (in intention, not fact) 15 years ago in 2009.

Well, my best wishes on that.  I had a look at your page and the stuff on 

dependent types is a step forward.

The integration should naturally extend Shen's logic and type systems to allow styles 

of dependently typed programming and theorem proving akin to those found in programming 

languages like Agda and Lean.

Mark, in recognition of what you're doing here, which is very difficult btw,  and something I

did not do, I'd like to extend the recognition of the Shen Open Science prize which consists 

of a free copy of TBoS.  Since TBoS is about to enter the final 5th edition, I'll hold back until 

the new copy is out and arrange for it to be sent to your address.

Again well done.

Mark

[Mark]

Thank you, I'm honoured.

[Mark]

Scryer Shen now supports types! I'll release a blog post detailing its ~ type equality operator soon.

[Joel McCracken]

OOC, Mark, what does Racket do in this project's architecture? Does racket do most of the code evaluation, and Scryer does the prolog evaluation (for prolog? etc calls) and type checking (which IIUC uses Shen prolog internally, tho I'm not entirely sure about that, still haven't completed the TBoS)

I recall interacting with you a little bit on the Racket discord group while you were developing this; at the time I thought that this was a self-education exercise, but I see that it has very interesting goals otherwise.

Would it be feasible to implement entirely in Scryer, bypassing any need for Racket? ofc this may have a variety of other impacts.

Joel

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/bba5af3c-fc30-4fcc-a172-a73f0c591795n%40googlegroups.com.

[Mark]

Racket is responsible for expansion and evaluation of all Shen forms while Scryer is responsible for evaluating Prolog queries directly issued to it from the prolog? form and indirectly from the type system. The whole system could be implemented in Scryer Prolog but at this point it's much more performant to do it from Racket (Scryer is a performant Prolog engine but not a performant Lisp engine). Racket has unique metaprogramming strengths in addition to being based on the very fast Chez Scheme implementation, so this makes the most sense to me ATM.

Scryer Prolog is run as a subprocess and communicates with the Shen image through standard IO. Translation between Shen syntax and ISO Prolog syntax is necessary to facilitate this, of course. At start time Scryer Shen opens a debugging window that echoes some of this interaction.

[Joel McCracken]

very cool. I wonder how e.g. racklog would perform vs scryer, in order to keep it all in a single tech.

To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/c45e615c-6082-45ce-8a7d-f1bd3a59bce8n%40googlegroups.com.

[Bruno Deferrari]

On Mon, Aug 12, 2024 at 7:50 PM Mark <markjor...@gmail.com> wrote:

Scryer Prolog is run as a subprocess and communicates with the Shen image through standard IO. Translation between Shen syntax and ISO Prolog syntax is necessary to facilitate this, of course. At start time Scryer Shen opens a debugging window that echoes some of this interaction.

Should be pretty easy for any Shen port to take advantage of Scryer Prolog then, right? That's great.

 

To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/c45e615c-6082-45ce-8a7d-f1bd3a59bce8n%40googlegroups.com.

--

BD

[Mark]

it would have to parse the strange dotted functor syntax I use to distinguish data from executable forms, but yes, it would be fairly easy.

[Mark]

I've posted the article: https://github.com/mthom/scryer-shen/wiki/Some-novel-features-of-Scryer-Shen