|
6macros: discussing the finer points of Perl 6 macros, Qtrees, and how to stay sane | irclog: irclog.perlgeek.de/6macros/today Set by moderator on 28 July 2015. |
|||
|
02:09
vendethiel joined
06:25
Ven joined
06:55
FROGGS joined
07:54
FROGGS joined
08:26
Ven joined
08:39
Ven joined
11:21
Ven joined
|
|||
| 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 | ||
| well | |||
| I'm afraid there's no way | 12:03 | ||
| I only looked very shallowly during my weird experiment, though :) | |||
| masak | I would be satisfied with it working only sorta-kinda | ||
| and with many caveats | 12:04 | ||
| Ven | if you think a way, keep me updated please | ||
| masak | will do -- it *feels* like it should work :) | 12:09 | |
| or rather, I *want* it to work | 12:10 | ||
| 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 | |||
| we could, worst case, do all the type checking as `where` clauses checking properties off of this object | 12:11 | ||
| that'd mean that the checking would happen at runtime, which would be sad but still kinda work | |||
| it'd mean you'd actually have to run your proof, not just compile it | |||
| masak finds that he gets more interested in dependent types (and homotopy) day by day | 12:12 | ||
| Ven has been doing ASM and APL, and finds that his brain is numbly biased towards those | 12:13 | ||
| masak | so typeless | ||
| Ven | :P | ||
| 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 | ||
| it's a totally different area, other school of thought anyway | |||
| masak | I think there's a CS elite who think of "typed" as meaning "statically typed" or "Hindley-Milner" or somewhere in-between | ||
| this creates a bit of friction with the rest of the world | 12:15 | ||
| I've never really engaged with that debate, to be honest | |||
| 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. | |||
| 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 | ||
| test what your types don't provide. seems fair. | |||
| masak | yeah | ||
| then again | 12:17 | ||
| in the weekend, I was translating a toy project of mine from JS to TS | |||
| found bugs. | |||
| Ven | (I never engaged in such discussions either – or at least, the only time I did, I quickly disengaged) | ||
| masak | just by the IDE telling me things didn't typecheck/compile | ||
| Ven | (I'm afraid I'd end up talking with people like tonymorris/dibblego) | ||
| masak | so, I dunno. it's a debate where both sides have a point. | ||
| Ven | oh, sure | 12:19 | |
| I mean – it's because perl6 has types I like it so much ;) | |||
| the cool thing is -- even if perl6 turns out to be a disaster in itself as a language | |||
| we'd still have enough tools to get the same power (MOP, macros, coroutines, ffi, etc) to build something on top of it :) | |||
| masak | \\o/ | 12:23 | |
| lose-win! :D | |||
| for me, Perl 6 is all about the journey, not so much about the final product | |||
| Ven | well, there a few areas I don't like in perl6. flattening is one such. but I mostly totally love it. | 12:26 | |
| masak | nod | 12:27 | |
| Ven | I don't pretend I know.. | ||
| 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:31 | |
| Ven | did you see github.com/jozefg/learn-tt ? | 12:32 | |
| masak | no, I don't believe I did. Ven++ | 12:33 | |
| I re-opened TAPL the other day, though. it's a really really neat book. | |||
| Ven | never read it | 12:34 | |
| masak | it's jnthn's copy I have at home. he let me keep borrowing it when he moved. | 12:36 | |
| I think TAPL clocks in as having the same je-ne-sais-quoi as TAoCP for me | |||
| some combination of the author's deep knowledge of a subject, and a purity of expressing it in a book | 12:37 | ||
| there's no "cruft" | |||
| every new thing builds cleanly on things that were already introduced | |||
| it's both academic *and* very readable | |||
| Ven | ..interesting | 12:38 | |
| 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 | ||
| since then, I've picked up quite a bit of category theory | |||
| 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:40 | ||
| Ven | could be a win in my book :) | 12:42 | |
| brb for a bit | |||
| well, "right" back | |||
| masak thinks www.cse.chalmers.se/research/group/...k/book.pdf looks promising | 12:44 | ||
|
12:55
Ven joined
|
|||
| Ven | I'm *terrible* at logic | 12:56 | |
| I don't have the time for it | 12:57 | ||
| masak | not sure what to make of that :) | 12:58 | |
| logic is just programming, except you never hit "compile" :P | |||
| Ven | sure isn't! | 13:00 | |
| masak | logic is just math, but with only two numbers :P | 13:02 | |
| logic is just chess, but without the pieces, the board, the game itself, or the players | 13:03 | ||
| Ven sighs | 13:05 | ||
| *g* | |||
|
13:15
FROGGS joined
15:30
Ven joined
15:55
Ven joined
16:31
Ven joined
16:52
ilbot3 joined
18:09
vendethiel joined
20:24
vendethiel joined
20:30
Ven joined
|
|||