badkins has quit [Remote host closed the connection]
sze42 has joined #racket
lockywolf has quit [Ping timeout: 246 seconds]
ziyourenxiang has joined #racket
<lf94>
tautologico, ah ok then
<lf94>
tautologico, this conversation just made me think: if we add a rule that "a lambda variable cannot be used more than once", I think recursion/non-termination is impossible
badkins has joined #racket
lockywolf has joined #racket
lockywolf_ has joined #racket
lockywolf has quit [Ping timeout: 268 seconds]
bartbes has quit [Ping timeout: 268 seconds]
bartbes has joined #racket
pierpa has joined #racket
mzan has left #racket [#racket]
rnmhdn has joined #racket
ubLIX has quit [Quit: ubLIX]
badkins has quit [Remote host closed the connection]
<lf94>
sze42, so that guy just did what i mentoined?
<lf94>
made contracts obselete by storing more info in type
<sze42>
lf94: I guess, but his "type" isn't typed-rackets "type", its something build on top, a sort of "#lang typed/racket/fn"?
<sze42>
lf94: or maybe typed/racket could be extended to have a macro that does what he does but makes integrates it with the rest of its usual syntax?
<sze42>
lf94: I am just brainstorming I am a typed-racket noob :)
<lf94>
I'm even more noob
<lf94>
I dont even know racket at all :D
<lf94>
I came here because of personal lambda calculus study
<lf94>
as in, my studying has put me on a path where racket is a place along the way
<lf94>
not planned or anything - but from I gather, racket is the ultimate in programming language
<lf94>
for many reasons
<lf94>
but mostly because it is extremely close to lambda calculus itself - the ultimate abstraction of computation.
<sze42>
lf94: I use racket since quite a while but you always find new cool stuff and understand more, and realize that there is more to learn
<lf94>
almost all advanced concepts I've seen
<lf94>
this is crazy - almost all I've seen, are some variant of a simple lambda calculus idea.
<sze42>
lf94: racket is my default language, but from a theoretical point I also like smalltalk, mozart/oz, and someday have to explore typed things like idris
<lf94>
idris is nice theoretically too
<lf94>
but again: I think this will lead back to racket eventually.
<lf94>
I think you are ahead honest
<lf94>
honestly
<sze42>
idris with its dependent types theoretically is the middle point between racket and typed/racket except that you have to type instead of being able to choose to do it?
<lf94>
yes you must choose types
<lf94>
just like haskell
<lf94>
but you can enforce this in type/racket too
<lf94>
the one feature to me that is big, is 'holes'
<lf94>
Google brings up nothing in regards to racket
<lf94>
and holes
<lf94>
basically: the type system suggests what types will fit there
<sze42>
i think you can write dependent contracts in racket, but typed-racket not (yet?) supports dependent types
<sze42>
I am not sure if holes are very usefull in a language without dependent types, maybe, in general I haven't done much typed programming
badkins has quit [Remote host closed the connection]
dddddd has quit [Remote host closed the connection]
<sze42>
https://wiki.haskell.org/GHC/Typed_holes from reading the introduction it seems holes are always useful if the typesystem can add some information to that program location
badkins has joined #racket
bartbes has quit [Ping timeout: 250 seconds]
badkins has quit [Remote host closed the connection]
<jcowan>
specifically, mzscheme was the name not only of the language but of the CLI interpreter
<bremner>
the alias still exists, iirc
<jcowan>
as opposed to drscheme, mred, and various other jokes
<jcowan>
Not surprising
<jcowan>
When Chez was open-sourced there was a complaint that the REPL was called simply "scheme"
<bremner>
but probably only interesting to people with old scheme codebases
<jcowan>
which not only conflicts with MIT Scheme (which has priority) but also with people who want "scheme" to run their favorite Scheme
<jcowan>
Kent Dybvig replied that he had been starting the REPL by typing "scheme" for too long to retrain his fingers now (or words to that effect)
<jcowan>
It's already bad that "csc" is one Scheme compiler and "python" another, though I don't think the latter is actually a shell command
<jcowan>
again, the Scheme compilers have priority, but "the love and torrent of power prevailed"
pierpal has joined #racket
dbmikus has joined #racket
handicraftsman has left #racket ["Leaving"]
jao has quit [Ping timeout: 245 seconds]
<lavaflow>
does racket have a procedure equivalent to srfi-1's zip anywhere?
<lavaflow>
I mean, other than requiring srfi-1
<lavaflow>
I don't know if it's justified, but I try to avoid the srfi's when using racket. I think they're named in a way that makes code difficult to follow.
<bremner>
lavaflow: you could (map list lst1 lst2 ... lstn)
<lavaflow>
that doesn't seem to quite work. it works with the map from srfi/1 but not the map from racket/base
<lavaflow>
"; map: all lists must have same size" <- from racket/base's map
<lavaflow>
but srfi/1's map does it fine
<lavaflow>
I wonder why racket's map is more restrictive.
ym has joined #racket
<bremner>
oic, I missed that.
<lavaflow>
I thought it worked at first too because I'd already included srfi/1 in my repl, but then when I ran it outside my repl it didn't work :)
dddddd has quit [Remote host closed the connection]
<lf94>
I am having an issue though...in that, can't all this be expressed with regular lambda?
<lf94>
One difference between a normal lambda and a slot lambda is that you can pass a slot lambda to
<lf94>
obtain a new slot lambda with an intuitive result:
<lf94>
(1 + _)(_ + _) = (1 + (_ + _))
<lf94>
------
<lf94>
But if you change the reduction method in regular lambda you can do just the same. call-by-name.
<johnjay>
lf94: where did you learn lambda calculus from? i'm looking for a book
<lf94>
the internet
<lf94>
:v
<johnjay>
ok
<johnjay>
trick question i guess, since i have an open tab i just haven't looked at which discusses it.
<johnjay>
old Flagg.pdf, you have survived many crashes and firefox-losing-all-sessionstore-data incidents
endformationage has joined #racket
pera has quit [Ping timeout: 245 seconds]
pera has joined #racket
<lf94>
lol
<johnjay>
that's why i gave up on having large numbers of tabs by the way.
<johnjay>
not for any logical reason, but just because firefox had no reliable way to save them
<lf94>
I never have more than 7 open
<lf94>
because: focus
<johnjay>
even better, I have an extension to cap my number of tabs at 16
<johnjay>
because: laziness
<sze42>
I have never fewer than 7 open, because: distraction XD
dbmikus has quit [Ping timeout: 272 seconds]
rnmhdn has joined #racket
dbmikus has joined #racket
<lf94>
master focus, it will help a lot :)
<tautologico>
johnjay: if you want a book, I'd recommend Types and Programming Languages by Pierce which starts with untyped lambda calculus and then proceeds to introduce a lot of type systems and theory
<lf94>
This like simplifies the core idea of homotopy theory
<lf94>
love it
<lf94>
paths are the universe
<lf94>
B)
dvdmuckle has quit [Quit: Bouncer Surgery]
dvdmuckle has joined #racket
mahmudov has joined #racket
<lf94>
Could someone actually help me understand that equality definition?
<lf94>
I have no idea how to read it properly
<lf94>
or read it meaningfully.
sauvin has quit [Remote host closed the connection]
<sze42>
lf94: seems like chasing the silver bullet to me, fun to try to find something general, but it is very abstract, maybe useful for constraint solvers, theorem provers etc. but I don't know what to do with it
<sze42>
lf94: if I want a nand gate I use one and look what can do from there
ziyourenxiang has quit [Ping timeout: 246 seconds]
<sze42>
lf94: I think equivalence can be very useful, but I think that equivalent implementations of a common interface are often enough
dddddd has joined #racket
<lf94>
sze42, yeah.
<lf94>
I just love the idea of building all mathematics out of it
<lf94>
to me it screams "lamda calculus was right"
<lf94>
because of how they use the idea of nand gate
rnmhdn has quit [Ping timeout: 240 seconds]
<lf94>
I am definitely going to start building my own languages I think
<lf94>
I am starting to see the usefulness
<lf94>
all programs are just state machines, and a language specific to manipulating this state machine should be easy to use
<sze42>
lf94: well lots of things are turing complete and lambda calculus is a good one because it is small and useful, but I am definitely leaning more towards a language that is practical and allows me not having to be smarter than necessary
<sze42>
its fun to do clever things and then you build something cool until you can't fit in your head anymore and then you stop working on it because it breaks your brain
<sze42>
at least thats how I felt sometimes in the past
pera has quit [Ping timeout: 246 seconds]
<sze42>
but I guess it is a good exercise and one should try to exceed believed limits, so really it depends on what your goal is
<lf94>
to me it is 'higher order thinking'
meepdeew has joined #racket
pera has joined #racket
johnjay has quit [Disconnected by services]
meepdeew has quit [Remote host closed the connection]
pera has quit [Ping timeout: 246 seconds]
ubLIX has joined #racket
pierpal has quit [Read error: Connection reset by peer]
pierpal has joined #racket
jao has joined #racket
ATuin has joined #racket
ng0 has quit [Remote host closed the connection]
ng0 has joined #racket
ZombieChicken has joined #racket
fernando-basso has joined #racket
Sgeo_ has quit [Ping timeout: 250 seconds]
Sgeo has joined #racket
pie___ has joined #racket
pie__ has quit [Remote host closed the connection]
g00s has joined #racket
<jcowan>
I just use extra tabs as a todo list
<jcowan>
(on Chrome, where they are pretty reliably saved, the only problem being that if you fail to click the button in the "Restore tabs?" dialog box, they are LOST FOREVER
fmnt has joined #racket
sze42 has quit [Quit: Leaving.]
pera has joined #racket
fmnt has quit [Client Quit]
libertyprime has joined #racket
dbmikus has quit [Quit: WeeChat 2.3]
ATuin has quit [Quit: WeeChat 2.3]
sleepnap has left #racket [#racket]
pie___ has quit [Remote host closed the connection]