Perl 6 - the future is here, just unevenly distributed

IRC log for #6macros, 2015-09-30

| Channels | #6macros index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
02:09 vendethiel joined #6macros
06:25 Ven joined #6macros
06:55 FROGGS joined #6macros
07:54 FROGGS joined #6macros
08:26 Ven joined #6macros
08:39 Ven joined #6macros
11:21 Ven joined #6macros
12:02 masak Ven: do you know if there's any sensible way to do propositions-as-types in Perl 6?
12:02 Ven I'm afraid no
12:02 Ven well
12:03 Ven I'm afraid there's no way
12:03 Ven I only looked very shallowly during my weird experiment, though :)
12:03 masak I would be satisfied with it working only sorta-kinda
12:04 masak and with many caveats
12:04 Ven if you think a way, keep me updated please
12:09 masak will do -- it *feels* like it should work :)
12:10 masak or rather, I *want* it to work
12:10 masak what's the lamest thing that would still qualify? I mean, if we didn't do any type-checking at all, we could still talk about propositions as objects
12:11 masak we could, worst case, do all the type checking as `where` clauses checking properties off of this object
12:11 masak that'd mean that the checking would happen at runtime, which would be sad but still kinda work
12:11 masak it'd mean you'd actually have to run your proof, not just compile it
12:12 * masak finds that he gets more interested in dependent types (and homotopy) day by day
12:13 * Ven has been doing ASM and APL, and finds that his brain is numbly biased towards those
12:13 masak so typeless
12:13 Ven :P
12:14 masak not even *un*-dependently typed :P
12:14 Ven I know how tons of people say scripting languages are "untyped", but I find this pretty stupid
12:14 Ven it's a totally different area, other school of thought anyway
12:14 masak I think there's a CS elite who think of "typed" as meaning "statically typed" or "Hindley-Milner" or somewhere in-between
12:15 masak this creates a bit of friction with the rest of the world
12:15 masak I've never really engaged with that debate, to be honest
12:15 masak I like TDD. I like some kinds of typing. I don't see them being in competition or a zero-sum game or mutually exclusive.
12:16 masak I do notice that when I'm in one of 'em dynamic languages, I lean much more heavily on TDD for things I would have leant on the type system for in more static languages
12:16 Ven "you need tests to the extent you do not have type" is a sentence I like
12:16 Ven test what your types don't provide. seems fair.
12:16 masak yeah
12:17 masak then again
12:17 masak in the weekend, I was translating a toy project of mine from JS to TS
12:17 masak found bugs.
12:17 Ven (I never engaged in such discussions either – or at least, the only time I did, I quickly disengaged)
12:17 masak just by the IDE telling me things didn't typecheck/compile
12:17 Ven (I'm afraid I'd end up talking with people like tonymorris/dibblego)
12:17 masak so, I dunno. it's a debate where both sides have a point.
12:19 Ven oh, sure
12:19 Ven I mean – it's because perl6 has types I like it so much ;)
12:19 Ven the cool thing is -- even if perl6 turns out to be a disaster in itself as a language
12:19 Ven we'd still have enough tools to get the same power (MOP, macros, coroutines, ffi, etc) to build something on top of it :)
12:23 masak \o/
12:23 masak lose-win! :D
12:23 masak for me, Perl 6 is all about the journey, not so much about the final product
12:26 Ven well, there a few areas I don't like in perl6. flattening is one such. but I mostly totally love it.
12:27 masak nod
12:27 Ven I don't pretend I know..
12:31 masak Ven: where can I read more about dependent types in order to deepen my understanding? I'm tired of the simple examples like natural numbers or lists with a typed length. I suspect there is richer food out there that I don't know about.
12:32 Ven did you see https://github.com/jozefg/learn-tt ?
12:33 masak no, I don't believe I did. Ven++
12:33 masak I re-opened TAPL the other day, though. it's a really really neat book.
12:34 Ven never read it
12:36 masak it's jnthn's copy I have at home. he let me keep borrowing it when he moved.
12:36 masak I think TAPL clocks in as having the same je-ne-sais-quoi as TAoCP for me
12:37 masak some combination of the author's deep knowledge of a subject, and a purity of expressing it in a book
12:37 masak there's no "cruft"
12:37 masak every new thing builds cleanly on things that were already introduced
12:37 masak it's both academic *and* very readable
12:38 Ven ..interesting
12:39 Ven well. it's very vague when you say it, of course :)
12:39 masak I read through about half of it some eight years ago
12:39 masak since then, I've picked up quite a bit of category theory
12:40 masak and now as I come back to it, I can see that the author knows CT quite well, though he never spells it out, and he's never tempted to invoke CT concepts just because
12:42 Ven could be a win in my book :)
12:42 Ven brb for a bit
12:42 Ven well, "right" back
12:44 * masak thinks http://www.cse.chalmers.se/rese​arch/group/logic/book/book.pdf looks promising
12:55 Ven joined #6macros
12:56 Ven I'm *terrible* at logic
12:57 Ven I don't have the time for it
12:58 masak not sure what to make of that :)
12:58 masak logic is just programming, except you never hit "compile" :P
13:00 Ven sure isn't!
13:02 masak logic is just math, but with only two numbers :P
13:03 masak logic is just chess, but without the pieces, the board, the game itself, or the players
13:05 * Ven sighs
13:05 Ven *g*
13:15 FROGGS joined #6macros
15:30 Ven joined #6macros
15:55 Ven joined #6macros
16:31 Ven joined #6macros
16:52 ilbot3 joined #6macros
18:09 vendethiel joined #6macros
20:24 vendethiel joined #6macros
20:30 Ven joined #6macros

| Channels | #6macros index | Today | | Search | Google Search | Plain-Text | summary