This page is not created by, affiliated with, or supported by Slack Technologies, Inc.
2018-02-11
Channels
- # beginners (79)
- # boot (21)
- # cider (28)
- # cljs-dev (1)
- # clojure (88)
- # clojure-italy (3)
- # clojure-russia (6)
- # clojurescript (49)
- # community-development (4)
- # cursive (37)
- # datomic (12)
- # editors (3)
- # emacs (33)
- # fulcro (15)
- # hoplon (9)
- # jobs-discuss (3)
- # keechma (3)
- # lein-figwheel (2)
- # luminus (3)
- # off-topic (146)
- # onyx (5)
- # portkey (11)
- # re-frame (34)
- # reagent (7)
- # reitit (5)
- # remote-jobs (1)
- # shadow-cljs (6)
- # unrepl (11)
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
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?
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 ?
@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.
I'm trying to formalize what that means.@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
@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"
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 🙂
https://github.com/hraberg/shen.clj looks out dated, what are you running shen on?
in sequent calculus, how do these two differ: A1, ..., a_n |- B |- (A1 and A2 ... and A_n) -> B
but the first is a statement in the meta language, the other is a statement in the object language
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?
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.
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
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.
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))
that's pretty coollooks a lot like ml code
i do wish that clojure had arities on pattern matching of args and not just the number of args.
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
@dpsutton I'm a big fan of pattern matching like that, but I think it also takes good TCO.
I really love this syntax:
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 ^^
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
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
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 😄)
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.
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
many are aiming for r7, eventually at least
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.