it's quite ironic how he accuses clojure of not having done the proper research yet his claims about lux's macro system having new features that other lisp macro system don't have is just plain wrong

lux reminds me of shen in that both are interesting looking languages that I want to understand but have never had the time to play with

all that shen and lux have in common is they are lisps :)

shen is really cool

doesn't shen have a type system too?

it essentially has a theorem prover based on sequential calculus

not a conventional type system

and it's optional

There's nothing stopping anyone from writing macros as monads, I just don't quite know why I'd need that, and the documentation doesn't explain it. It's not like macros should modify the compiler in any meaningful way.

is the sequential calculus part of the lambda cube, or something completly outside of it?

nothing to do with it

sequent calculus is (being a bit vague here) a style of expressing derivation rules in a logic system

it looks like that [s0, s1, s2, ..., sn] is meant to say: for every i: (s0, s1, ..., s_{i-1}) -> s_i ?

or am I completely missing the point

I don't know what you just wrote is supposed to mean

@tbaldridge besides "Template Haskell probably uses Monads", I don't see the connection between Macros and Monads.

@bronsa: the first paragraph of wikipedia says:

Sequent calculus is, in essence, a style of formal logical argumentation where every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the style of natural deduction used by mathematicians than David Hilbert's earlier style of formal logic where every line was an unconditional tautology.

that wikipedia page is quite longer than just the first paragraph for good reasons

keep reading

@qqq the connection is "macros often need to parse their arguments", "certain monads can be used for parsing", so lux uses a monad for that

but there's no inherent connection between macros and monads

and that doesn't mean that macros are monadic like the author implies

it's a bit of an abuse of the term

@bronsa: lol, I think my learning style of "trying to grasp the main idea first + read the details later" is really annoying your style of "read the entire doc cover to cover first" 🙂 [re sequent calculus / jvm spec / types ]

my learning style is "try to learn, ask questions if I don't understand", not "ask questions to avoid having to read"

which I think scales a bit better than yours ;)

I can see how, from your perspective, trying to "get minimal example working / grab main idea" before reading entire docs, appears as "trying to avoid having to read"

for example, for this sequent calculus, what I really want rigt now, is some clojure impl, so I can play with it in a repl 🙂

you have an implementation in shen, you can try using that

https://github.com/hraberg/shen.clj looks out dated, what are you running shen on?

it doesn't matter

any implementation of shen will do

it doesn't care which host you use it on

I personally use the sbcl impl

in sequent calculus, how do these two differ: A1, ..., a_n |- B |- (A1 and A2 ... and A_n) -> B

you can derive one from the other

but the first is a statement in the meta language, the other is a statement in the object language

https://math.stackexchange.com/questions/286077/implies-vs-entails-vs-provable

from what I'm reading, sequent calculus is a way to prove things in propositional calculus, where A1 A2 ... A_n |- B_1 ... B_m means (and A1 A2 ... A_n) implies (or B_1 ... B_m) from which we get the following inference rules: https://imgur.com/a/vG2gu in practice, how does make Shen interesting (as opposed to say, having this as a library) ?

have you ever seen another language that uses an open logic calculus in place of a type system?

you can add any theorem or axiom that you want

you can do IO in the derivation rules

you can trivially achieve the levels of power that dependent types give you

you can also easily shoot yourself in the foot and make the logic inconsistent

lots of cool stuff, probably not practical at all

but hardly uninteresting

I've used Coq / Idris in the past; recently implemented STLC + three extensions to get it to the Calculus of Constructions. I don't understand Dependent types. These "inference rules" , when squinting, looks like type inference rules, but it's not obvious to me what new power sequent calculus unleashes here.

in a type system, you have a defined logic and defined inference rules

in shen you have a do your own type system essentially

if you want subtyping, add the correct rules and you get it

Also, if sequent calculus only does propositional logic, can it type functions like: vec-concat :: [vec of len n] -> [vec of len m] -> [vec of len (m+n)] for taht, it seems like at min we need: data Nat = Zero | Successor Nat + quantifiers

there's lots of other interesting stuff in shen other than the "typing system"

it's got an embedded prolog

a yacc parser

powerful pattern matching with explicit backtracking

etc etc

http://www.shenlanguage.org/learn-shen/index.html

this is a genuine practical question: does sequent calculus make it easy to reason about dimensions of vectors / matrices ? the driving motivation behind the JVM bytecode generation is something num-clj like, -- and if possible, II want to be able to statically detect dimension mismatches

there's nothing inherent to sequent calculus about that, the fact that you can do it in shen is because you can do arbitrary computation in derivation rules

@bronsa : 1. It's not obvious to me if this can be expressed in sequent calculus at all (I think it requires more than prop logic as it requires addition / subtraction, floor, ceiling, division by constant) 2. I don't know what 'you can do arbitrary computation in derivation rules' means, but it seems like I could make the really bad analogy of "you can do arbitrary computation in macros" 3. The impression I'm getting now is: it can't be done in sequent calculus, but it can be done in shen, becanse you can run arbitrary code at type inference time.

yes

the shen "type system" is intentionally turing complete

I'm not (yet) cynical as many things impossible in theory have easy instances in practice. A cynic would then cite https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems and say: look, if you add in derivation rules that encodes basic +-*/ , you get undecidable systems -- which means you (as the programmer) have to now also write a "theorem prover / checker" for the new derivation rules you've added. At this point, Shen's type system becomes: yes, sure, you ca type check arbitrary complicated things but you have to write your own derivation rules + theorem prover / checkers for those rules and at this point it's not clear what it really provides

I've said a while ago that shen allows you to make the logic inconsistent if you're not careful

and I also said that I don't think shen is practical at all, just extremely interesting

music!

user=> (clojure.pprint/pprint
  #_=>  (take 13
  #_=>        (iterate #(* % (Math/pow 2 (/ 12.0)))
  #_=>                 440.0)))
(440.0
 466.1637615180899
 493.8833012561241
 523.2511306011974
 554.3652619537443
 587.3295358348153
 622.253967444162
 659.2551138257401
 698.456462866008
 739.988845423269
 783.9908719634989
 830.6093951598906
 880.0000000000003)
nil
user=> 

You can play that in Supercollider via Sam Aaron’s overtone:

(use 'overtone.live)

(definst metal-bell [freq 220 dur 1.5]
  (* (squared (line 1 0 dur))
     (reduce + (map (fn [[amp f]] (* amp (sin-osc (* freq f))))
                    '((1 1)
                      (0.5 43/22)
                      (0.3 25/22)
                      (0.3 33/22))))))

(let [metro (metronome 180)
      beat (metro)]
  (map-indexed
   #(at (metro (+ beat %1))
        (metal-bell %2 1.0)) 
   (take 13 (iterate #(* % (Math/pow 2 (/ 12.0))) 440.0))))

from shen

(define foldl
       F Z [] -> Z
       F Z [X | Xs] -> (foldl F (F Z X) Xs))

looks a lot like ml code

yeah it's a strange blend due to the pattern matching being baked in

i do wish that clojure had arities on pattern matching of args and not just the number of args.

(define prefix?
  [] _ -> true
  [X | Y] [X | Z] -> (prefix? Y Z)
  _ _ -> false)
prefix?

core.match can do that, but the syntax is not nearly so elegant

yeah. but i think you have to be wary of method sizes becoming to large due to the expansion. also it can't do it in the signature but only in the body of the function

ultimately no big deal. just would be nice

@dpsutton I'm a big fan of pattern matching like that, but I think it also takes good TCO.

I really love this syntax:

yeah it's for sure interesting

i think i've seen a video on it. maybe someone presented at strange loop a few years ago?

i also like the prolog built right in. makes it more tempting to use. haven't taken a dependency on core.logic in the past

(defn count
  lst -> (count lst 0)
  [] cnt -> cnt
  [_ | R ] cnt -> (count R (inc cnt)))

Erlang style, syntax could use some work ^^

are you reading/learning anything interesting right now?

Eh, I've been playing around with trying to get efficient effect systems in VMs via delimited continuations. So I have half a dozen half-baked VMs that do that to some extent

i've never stayed with a scheme long enough to learn continuations

do you do any open source play things? i've seen some of brandon blooms experiments in interpreters online

I've been learning guile scheme, including someone's fix of scsh to work with guile 2.2 - scsh is a fascinating little dsl, and the level of direct unabstracted access from guile to OS level stuff on *nix is fascinating

are any of those vms on github or anything?

that sounds pretty neat. my scheme is superficial so i've never run into the differences between chez chicken guile, and others

check out this dsl https://gist.github.com/noisesmith/06102f38f14bad40ebe4a04f79f5dfda

>, /, &, ||, | etc. are all supported in the run macro as well (as prefix operators, naturally 😄)

are either of yall gonna be in new orleans next week for clojure sync by the way?

no, sounds interesting though

i'm right up the road from nola so i'm stoked to be there. and hotel prices are fairly cheap since its two days after mardi gras

@dpsutten So this is a bit different than normal continuations. Imagine that you had something that looked like a protocol:

(defhandler IState
  (get-state [this k])
  (apply-state [this f args k]))

(defrecord State [data]
  (get-state [this k]
    (k data))
  (apply-state [this f args k]
    (with-handler (->State (apply f data args)) k)))

(defn do-something [x]
  (if (< (get-state) 10)
    (apply-state inc)
    x))

The idea here is that when you call a defhandler method, the VM takes everything from that handler to the top of the call stack, and hands it as a function to the handler.

So what you see here is something a lot like the state monad in that you have 100% pure code, but without monads. I don't like monads because the pollute the return type of my functions, so this avoids those problems.

The key is this line: (with-handler (->State (apply f data args)) k)))

Every time you call apply-state the current handler replaces itself with a new handler, then "splices" the rest of the program back into place.

the k is "the rest of the program"?

right

so that's the difference though. When you use call-cc the k is the entire rest of the program.

In this case it's a delimited continuation, so k is only for the current execution point up to the handler being called.

It's a lot like bindings in clojure that way.

Anyway, if you have these sort of handlers and TCO, you can write execptions, core.async go blocks (that support stuff like higher order functions), generators, the state monad, lightweight threads, test.check style generators that are a bit more sane, a ton of stuff.

Sadly almost no VM on the planet supports this sort of construct.

A Ocaml based language that does all this and inspired me: http://www.eff-lang.org/

it seems like with that kind of effect handler system you could dependency inject anything that does side effects without needing to lift it to a procedure argument

(and pass it down through scope etc.)

That's pretty much the idea, it can really do anything monads do, without the typesystem side-effects of monads

nice, I could see that simplifying a lot of things if it worked efficiently

oh @noisesmith how are you learning guile? reading code, book, blogs, etc

reading docs / looking at code / experimenting in a repl

specifically reading the guile-scsh port code

the specific docs being the guile manual, the srfi documents, and r7rs

👍

r7rs supports a syntax for symbols that most schemes (including guile) don't implement, sadly

Welcome to Racket v5.3.6.
> (define |foo| 1)
> |foo|
1
> (define |foo bar| 2)
> |foo bar|
2

it makes some very weird things possible though

> (define || 3)
> ||
3
> (define |(define foo 1)| 1)
> (+ |(define foo 1)| |(define foo 1)|)
2

most schemes are r5 plus whatever they feel like, right?

many are aiming for r7, eventually at least

https://stackoverflow.com/a/35166610

but partial implementations are much more common than full and strict ones for any of the standards afaik

Transcribing another Rich Hickey talk, "Clojure, Made Simple", and not sure if I am hearing something correctly, or if I am, what it means. Was hoping someone here might know. Link to a few sentences before the thing I don't understand: https://www.youtube.com/watch?v=VSdnJDO-xdg&feature=youtu.be&t=46m39s

Here is what I think he is saying starting at that point: "And then in Clojure we have something called core.async which is a channel model. It is a little bit richer than queues, because you don't have to set up the threads and do all the micro writes."

Is "micro writes" what he is saying there? What does that mean?

@andy.fingerhut that's what I hear too, not sure what he means by that tho

interesting hacker news thread of david nolen's sudoku solver in core.logic. great summary explaining why logic is so neat in one of the comments https://news.ycombinator.com/item?id=4325746

https://news.ycombinator.com/item?id=16353966 <-- this is insane

at this point I don't even find things like that surprising

Crypto-level security when real money is at stake is not only "not for amateurs", it is also "not for people who have read through Applied Cryptography, done all the exercises, think they know what they are doing, but haven't broken actual system security for fun and profit before."

I am not such a person, but I think there is a parallel here to James Randi's observation that it takes a con man to catch a con man -- don't send research scientists to try to unmask Uri Geller.

@qqq I see server code trusting client code all the time, the problem with defense side security is the defender needs to do everything right every time, the attacker only needs to succeed once

FYI, a documentary titled "An Honest Liar" about James Randi is highly recommended, if you are even a bit interested in things like that.

The more I read about the crypto-currency stuff, the less I want anything to do with it. It seems that the owner of BitGrail already violated their own TOS and implemented mandatory verification locking people out of the exchange so they couldn't get their own money out. Seems like a lot of unethical and/or clueless people are involved in that industry.

A lot of "get rich quick" folks. And, frankly, they deserve to get stiffed.

@noisesmith: I don't think I've ever written production server code that trusts client code; but at the same time, there's not lots of motivated hackers attacking my code daily.

One of my favorite sections of Rich's talk "Clojure, Made Simple" (see announcements channel for link to transcript and video), where he briefly describes his personal journey away from Java/C++/C# to Lisps, and creating Clojure: "So the idea behind Clojure, or one of the ideas behind Clojure, is just this. I had done so much object-oriented programming, and it is just so much busy work and so much extra stuff. And when I finally, later in my career, learned Lisp, I saw people building very very interesting systems out of much much simpler stuff. And I tried it, and guess what? You can build exactly the same systems out of much much simpler stuff. And I said -- well, I cannot repeat it. But I was very unhappy. Basically, something to the effect of: I have been wasting my time and my career doing what I have been doing. I need to do something. I need to change what I am doing. Because I am wasting my time. I am wasting my life doing it this way."

Yeah, I learned Lisp and APL as an undergraduate, then did three years PhD work on FP... and then had to program in C, C++, and Java for a living. I totally sympathize with Rich's position on that...

...you're plugging away at your day job and you're constantly thinking "I know there's a better way to do this!"... but the better way just doesn't get traction in industry. Nice to things improving now (finally!) and even the mainstream languages getting functional features.

crypto is a weird beast. it's a wild west. but if you have your money on an exchange at all then you are a chump.

never, ever, ever keep money on an excahnge. the whole point of crypto is that it's decentralized. treating an exchange like a bank is asking for exactly the kind of trouble that crypto was designed to eliminate.

new thing in crypto-land is atomic swaps: eliminate exchanges completely.

but as in any wild west, there will be scammers.