Aditya Siram: Shen Trick Shots - λC 2016

[Bruno Deferrari]

Here is the video of Aditya's talk at LambdaConf 2016:

https://www.youtube.com/watch?v=BUJNyHAeAc8

--
BD

[Mark Tarver]

The question about dependent types is a bit tricky. ' Does Shen handle dependent types?'  can be answered either affirmatively or negatively.  Let me quote myself in response to Mark Thom.

"... the sequent calculus in Shen allows you to formulate pretty much any type discipline you like; in fact as J. T. Gleason proved in 2007, Shen sequent calculus is a Turing equivalent notation in its own right.   However that does not mean you can prove anything you like even if what you are trying to prove is theoretically provable from the rules you give.

There are two reasons for that.  The first is that the Shen type checker (ATP) uses a fixed control mechanism - depth-first search with chronological backtracking - which it inherits from Prolog.  From TBoS chapter 20 you know that there are certain rules which create problems for that control mechanism where the ATP gets lost down an infinite branch.  The second is that Shen makes simplifying assumptions about the problems it is faced with; it assumes that the types of the functions it has to prove are, syntactically, the kind you would find in ML.  This does not prevent you formulating very exotic types - like the type of prime numbers etc.   .....

This simplifying assumption makes possible the T* algorithm which gives a good performance.    T* gave a factor of 7x in speedup over T - the predecessor.   Typically in ATP work if you can restrict the range of cases you are prepared to deal with, you can make optimisations in the proof process which make practical work possible.  This is the whole computational basis of logic programming. The very first Shen (Qi actually) ran under a 166MHz Pentium so this optimisation was very important given the limited computing power available in 1998.   The goal was to give fast and fully automatic type verification.

When you try to subvert this assumption then you need to rethink all this because with dependent types you begin the transition to interactive verification and formal methods and the changes are not trivial ....  So in short you can state anything you want but in practice you cannot prove anything you want."

Actually one of the plugins for SP uses dependent types in the formulation because Shen can operate with the concept of a dependent type quite comfortably.   In fact part of the type system uses them in a minor way.  What it cannot do is prove a function is dependently typed in part because the system is set up to store function types as simple signatures in the manner of ML.  

Mark

[Mark Tarver]

Here's an example; I want a dependently typed proof assistant that takes a type as an input and enforces that type on the inputs:

(datatype my-prover-types

Hyps : (list Type); P : Type;

______________________________

(myprover Type Hyps P) : boolean;)

I put a dummy function in

(define myprover

  Type Hyps P -> true)

Off we go.

(39+) (myprover symbol [p q r] p)

true : boolean

(40+) (myprover number [p q r] p)

type error

Mark

[Mark Tarver]

Interesting talk.  Just looking at the first 5 minutes.   Just a few notes.

1.  read-from-string is actually invoking the Shen reader on the contents of a string using Shen notation conventions.  So not surprisingly it will not read the string contents according to Json conventions.  I guess its a short cut though - to use the Shen reader and correct the output rather than write your own tokeniser.

2.  eval is horribly slow for such a small task.  And you don't really need Shen YACC for unconsing because really parsing is not needed here.

(54-) (define uncons

        [cons X Y] -> [(uncons X) | (uncons Y)]

        X -> X)

uncons

(55-) (read-from-string "{ c#34;a-keyc#34; : [1,2,3,4] }")

[{ "a-key" : [cons 1 [cons , [cons 2 [cons , [cons 3 [cons , [cons 4 []]]]]]]]

(56-) (map (function uncons) (read-from-string "{ c#34;a-keyc#34; : [1,2,3,4] }

[{ "a-key" : [1 , 2 , 3 , 4] }]

You can get rid of the commas too.

(57-) (define uncons+decomma

    [cons , Y] -> (uncons+decomma Y)

    [cons X Y] -> [(uncons+decomma X) | (uncons+decomma Y)]

    X -> X)

uncons+decomma

(58-) (map (function uncons+decomma) (read-from-string "{ c#34;a-keyc#34; : [1,2,3,4] }"))   

[{ "a-key" : [1 2 3 4] }]

Mark

[Mark Tarver]

Another note - at 4:50 - you have {} and {   } as separate cases in your <object> definition.   Actually because you are using the Shen reader, you don't need both cases.  Shen puts in the white space automatically, treating { and } as tokens. This is so Shenturians don't have to worry about the difference between

(define foo

   {boolean --> boolean}

...)

and

(define foo

  { boolean --> boolean }

...)

which would otherwise drive people nuts.  e.g.

(69-) (= [{}] [{ }])

true

 

Mark

--
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+unsubscribe@googlegroups.com.
To post to this group, send email to qil...@googlegroups.com.
Visit this group at https://groups.google.com/group/qilang.
For more options, visit https://groups.google.com/d/optout.

[deech]

I definitely didn't need to use `defcc` for parsing out JSON. And yes, using the Shen reader is an awful hack, but it was convenient. The idea was to expose the audience to Shen-YACC in a familiar domain. I later use it more as intended.

[Mark Tarver]

10:18  You have ((function modify) (fold-lenses <chain-lenses>)).  Isn't (modify (fold-lenses <chain-lenses>)) enough here?

13:31  You say that *store* : (list coin) in your axioms; surely you mean (value *store*) : (list coin)?

Mark

[deech]

Also, in case you don't want to read code off the slides, I have executable examples here: https://github.com/deech/lambdaconf-shen-talk.

To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.

[deech]

(1) Yes that (function ...) call was probably unnecessary.
(2) Here's the complete datatype (https://github.com/deech/lambdaconf-shen-talk/blob/master/Typed-Coins.shen#L11). It seems to typecheck.
-deech

[Mark Tarver]

I believe you; but unfortunately your axioms pass (head *store*) as type secure which you don't want.  What you need is:

(datatype coin

  if (element? Coin [penny nickel dime quarter])

  ___________

  Coin : coin;

  

  ____________________

  (value *store*) : (list coin);)

(define insert-coin

  {coin --> (list coin)}

  Coin -> (set *store* (append (value *store*) [Coin])))

  

 Mark 

--

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+unsubscribe@googlegroups.com.

[deech]

Yes, of course. Ugh.

To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.

[Mark Tarver]

These things happen, don't let it kill you; btw I'm happy to preview stuff if you need it.

12:36 " [A Shen] datatype form [is] broken up by what is called 'sequents'"

Well, not really.  I think what you mean is that Shen datatypes are specified by sequent calculus rules.  That's what you are pointing at on the slide.  Sequents are (in single conclusion calculus that Shen uses) pairs composed of a list of assumptions and a conclusion.  Sequents are manipulated by datatype rules to be sure.   The general explanation is fine thereafter. 

Mark

[deech]

You're right but I was referring how it's broken up syntactically. I specifically chose this phrasing because a later example shows how to build up a datatype at runtime. I'll certainly take you up on your offer next time. I was a bit behind for this talk.
-deech

[Mark Tarver]

Yes; sure. You have some redundancies in the code.

(defcc shen.<strc>

  Escaped Byte := (n->string Byte) where (= Escaped 92);

  Byte := (n->string Byte) where (not (= Byte 34));)

  

is just  

(defcc shen.<strc>

  92 Byte := (n->string Byte);

  Byte := (n->string Byte) where (not (= Byte 34));)

(defcc <object>

  { <members> } := [object | <members> ];

  {}            := [object];

  { }           := [object];)

  

is just  

  

(defcc <object>

  {<members>} := [object | <members>];

  {}          := [object];)

and

(defcc <array>

  [ <elements> ] := <elements>;

  []             := [];

  [ ]            := [];)

  

is just

(defcc <array>

  [<elements>] := <elements>;

  []           := [];)  

Mark

  

To unsubscribe from this group and stop receiving emails from it, send an email to qilang+unsubscribe@googlegroups.com.

[fuzzy wozzy]

I don't know what any of shen yacc is, and wouldn't know enough to follow the video if I tried,
but I sort of, in my own way, know what it's like to spend hours sometimes days making
what turns out to be simple programs, which for me at the time seemed monumentally hard,
and send to the forum, though it would be nice for other shenturians who are complete strangers
to make a comment or two, especially if encouraging and positive comments, but mostly I would eagerly
wait for dr. tarver to make a comment or two, hoping for encouraging if not all that positive of comments...

I can't quite remember, but I'm sure I've had a couple of halfway nice comments from dr. tarver back then,
or maybe I'm just imagining for my benefit, but then a barrage of bulleted comments disguised as criticism,
(or the other way around), would follow, what with his meticulous attention to details, even something seemingly
innocuous and (dare I say) unimportant as using the pattern matching rather than "where" as in the previous post,

while appreciative of the feedback and at the same time feeling like I let him down despite my best amateurish efforts
to make something to, if not to WOW him and other shenturians with, then I would've been ready to even take a meek
and lukewarm "wow...", but I would feel like I've once again wasted everyone's time and not feel like doing anything in
shen for a while, maybe for a good while... maybe just lacking passion in this overall, don't know...

but the presenter in the video did something no one here has been doing much lately, other than shen java's author
hakan raberg did, which is popularizing and making known shen to a wide group of people, via conferences and
videos and visual presentations, really, that takes time and effort, in terms of securing a spot in the conference enough
to attract some of the top programmers and managers in the industry, and to prepare the slides for visual presentation,
and if I were dr. tarver I would ask the presenter to show the shen code to me in advance so that all the little tweaks and
other nitpickable items can be ironed out way in advance, unless that's against the rules set by the conference itself?

in short, it takes lots of time and effort and preparation and sheer chutzpah, if you ask me, to stand in front of some of the
brightest group of programmers and show them and persuade them of the merits and importance of this still very young
and new language called shen... for that, I applaud the speaker, as well, I have no doubt, does dr. tarver, but what follows
after the fact, some corrections and criticisms, might hit the one who has worked so hard to make it happen, rahter cruelly,
of course that's the growing pain too, one does not become a shen master overnight, or even in 30 days, and I've all but
given up becoming even a shen apprentice especially in the field of "types", unless someone can sugarcoat it to make it easier
to use for the beginngers...

of course all the little tweaks and maybe even the big ones, who knows, I haven't watched the video, could be cleaned up if
dr. tarver himself were to give the presentation, but who knows, if enough people get interested, despite little quirks and
imperfections in the nooks and cranny of the presentation, the sponsors of the conference will eventually want to invite him too

they say patience is a virtue, but no one said that impatience is an eutriv...

[Mark Tarver]

Yes credit to Aditya for doing it and the stuff on lenses was interesting even though as a non-Json person, not easy to follow.  I have to correct some stuff in that presentation though when I put it up because it will otherwise misconceptions get rooted in people's minds.   I'm quite happy to preview anybody's code for a presentation.

Mark

[Mark Tarver]

dr. tarver himself were to give the presentation, but who knows, if enough people get interested, despite little quirks and imperfections in the nooks and cranny of the presentation, the sponsors of the conference will eventually want to invite him too

 

I'll answer that one.  Basically my time is paid for with one exception.  If people have a Shen problem with their home programming and they bring it here I'll help them for free.  I also clarify matters for people for free.  But I don't fly around the world on my own penny giving talks.  I haven't the money,  I haven't the time and I haven't the inclination.  If somebody wants to pay me to do something like that,  I'll do it.    The Milan talk in 2009 which introduced Shen was paid for.  Today I'd expect not only my expenses but the cost of my time.  

I'll support anybody who does it for love and I'll help him for free; no bother.   

Mark

[deech]

In my experience, unless you're a keynote or invited speaker your time will not be compensated. A lot of conferences, however, will cover your travel and boarding which was the case with this talk and the one at Strange Loop two years ago.

To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.

[fuzzy wozzy]

I cannot fathom it being done any other way,
2009 was a long time ago, has any sustainable interest been raised
among the participants since?

[Mark Tarver]

I was the invited speaker then, charged nothing for my time, and it still took 6 months with phone calls to get my expenses.  I resigned my membership of the Lisp committee. So I'm pretty clear about the conditions of my contribution now.   If I get called out, just like a plumber or any other regular guy, my time has to be respected.   

Back in 2009 Shen did not exist, Qi did, we had about 150 members in this group.  Now we have 500.  I look forward to more. Does this answer the question?  But this thread is about a talk by Aditya in 2016 and not one I gave in 2009; perhaps we should honour the title of the thread.

Well done Aditya;  the question on dependent types was hard to field.  Next time send me your slides and I'll be glad to spot any errors.

Mark

[deech]

I figured someone would ask about dependent types. I never presented myself as a Shen expert so I think "I don't know" was an ok response. The talk was more about highlighting some aspects of Shen that would be difficult to emulate in other languages. I'm still in the learning stage and perhaps only a step or so ahead of the total noob. In any case, it was well-received so I'd say (1) there is definitely quite a bit of interest in Shen and (2) there will be opportunities for further talks to delve into the more advanced Shen.

[Mark Thom]

Strange Loop will cover your boarding and travel costs if they approve your talk??

How was I not aware of this? I'd have submitted talks long ago.

[Mark Tarver]

I must say its a surprise for me too.   

Mark

On Thu, Sep 29, 2016 at 7:32 PM, Mark Thom <markjor...@gmail.com> wrote:

Strange Loop will cover your boarding and travel costs if they approve your talk??

How was I not aware of this? I'd have submitted talks long ago.

--
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+unsubscribe@googlegroups.com.

[deech]

Within the US I'm pretty sure they do. If you're travelling from abroad there might be a little more finagling involved but I'm not sure about that.

On Thursday, September 29, 2016 at 1:43:13 PM UTC-5, Mark Tarver wrote:

I must say its a surprise for me too.   

Mark

On Thu, Sep 29, 2016 at 7:32 PM, Mark Thom <markjor...@gmail.com> wrote:

Strange Loop will cover your boarding and travel costs if they approve your talk??

How was I not aware of this? I'd have submitted talks long ago.

--
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.

[Robert Herman]

Mark,

I am in full accord with you on your stance about compensation. I am also willing to help those doing things out of passion or love for a subject. It is not a logical contradiction, but a personal discrimination on my part, with the key being 'personal'; I decide,  and nobody decides for me.

I want to publicly thank Aditya for his talks. I have bought TBoS2E and TBoS3E, which has been written elsewhere are more like language specifications and some history. Aditya, or @deech's talks help me to see how I might actually apply Shen to things I want to develop, and get me actually coding and building muscle memory for Shen.

For example, the first talk Strange Loop with the web form demo is what set me to really focus on making Shen one of my useful languages rather than the others I mostly toy with, yet still with great fun (J, PicoLisp, Wasp Lisp). Shen on Ruby server side, and Shen for the JavaScript front end is an amazing synergy brought about by Shen's portability via KLambda. I don't even have to sacrifice Haskell with Mark Thom's Shentong!

Thanks to all for feeding my brain and my coding passions!

Rob

To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.

[Robert Herman]

Oh, forgot to mention the Shen/Emacs port also encourages my Shen studies, since I leave Emacs open all day!

[deech]

Wow, that's great feedback. Thanks!