←2014-07-07 2014-07-08 2014-07-09→ ↑2014 ↑all
00:00:27 -!- Bicyclidine has quit (Ping timeout: 255 seconds).
00:04:21 -!- conehead has joined.
00:07:26 <stickittothemain> or both?
00:13:11 -!- yorick has quit (Remote host closed the connection).
00:16:37 <stickittothemain> I'll start a github repo
00:16:48 <stickittothemain> it'll use python
00:17:12 <stickittothemain> just called ecic-eso
00:21:37 -!- stickittothemain has quit (Ping timeout: 246 seconds).
00:23:47 -!- stickittothemain has joined.
00:24:10 <Sgeo> I'd rather use whatever language I'm into at any given microsecond. If that means using Opa to make a BF interpreter, so be it
00:25:50 <Bike> shine on, you crazy diamond.
00:28:20 <stickittothemain> i don't really know git that well, how do you add contributers?
00:31:56 <stickittothemain> kind of an off topic thing for this channel
00:32:00 <stickittothemain> sorry
00:33:33 -!- Bike has quit (Ping timeout: 240 seconds).
00:35:46 -!- Bike has joined.
00:36:27 -!- clog has joined.
00:49:29 -!- Phantom_Hoover has quit (Quit: Leaving).
00:49:41 -!- nooodl_ has changed nick to nooodl.
00:55:18 -!- Bike has quit (Ping timeout: 240 seconds).
00:57:17 -!- Bike has joined.
01:32:54 -!- julio has joined.
01:33:14 -!- julio has left.
01:33:35 -!- not^v has joined.
01:57:22 -!- not^v has quit (Read error: Connection reset by peer).
01:57:48 -!- not^v has joined.
01:59:36 -!- not^v has quit (Client Quit).
02:23:59 -!- nooodl_ has joined.
02:24:44 -!- nooodl has quit (Disconnected by services).
02:24:48 -!- nooodl_ has changed nick to nooodl.
02:26:55 -!- conehead has quit (Quit: Computer has gone to sleep).
02:41:01 <Sgeo> "Our core interface is _not_ applicative or monadic, but more fundamental. It is monoidal, just like HTML itself!" Clearly, they need to write a monad wrapper for it for that nice do notation
02:46:06 -!- MoALTz_ has joined.
02:49:11 -!- MoALTz has quit (Ping timeout: 264 seconds).
03:33:12 -!- stickittothemain has quit.
03:48:56 -!- Speed`` has quit (Ping timeout: 264 seconds).
03:55:35 -!- rodgort has quit (Excess Flood).
03:56:03 -!- rodgort has joined.
03:56:31 -!- Speed` has joined.
03:57:34 -!- MoALTz_ has quit (Read error: Connection reset by peer).
03:59:09 -!- MoALTz has joined.
03:59:58 -!- clog has quit (Ping timeout: 240 seconds).
04:05:31 -!- nooodl has quit (Quit: Ik ga weg).
04:31:48 -!- Melvar` has joined.
04:33:36 -!- Melvar has quit (Ping timeout: 255 seconds).
04:34:03 -!- idris-bot has quit (Ping timeout: 240 seconds).
04:47:19 <Sgeo> (In a paper regarding Idris):
04:47:24 <Sgeo> "This project made no use of human subjects or external data. As such, there were no ethicalconsiderations for this project and accelerated ethical approval was sought."
04:52:30 <Bike> CS papers need ethical approval?
05:00:47 <pikhq> Bike: Not unless they use human subjects.
05:01:10 <pikhq> That was just a "fuck you" at Facebook, for using human subjects without consent and somehow getting it past an ethics board.
05:01:35 <Bike> oh. understandable. i thought that was socio psych something, though.
05:04:09 <Sgeo> Um. I don't think a paper written April 4th would have such a "fuck you"
05:04:25 <Sgeo> http://www.simonjf.com/writing/bsc-dissertation.pdf
05:06:07 -!- oerjan has joined.
05:09:26 -!- clog has joined.
05:11:18 -!- oerjan has set topic: The clogged channel | brainfuck survey: https://www.surveymonkey.com/s/L82SNZV | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/.
05:25:16 -!- not^v has joined.
05:35:38 -!- not^v has quit (Quit: http://i.imgur.com/Akc6r.gif).
05:53:24 -!- conehead has joined.
06:04:42 -!- oerjan has quit (Quit: leaving).
06:14:24 -!- Sorella has quit (Quit: It is tiem!).
06:22:26 -!- MoALTz has quit (Quit: Leaving).
07:10:54 -!- AnotherTest has joined.
07:19:45 -!- AnotherTest has quit (Ping timeout: 256 seconds).
07:38:07 -!- AnotherTest has joined.
07:43:30 -!- MindlessDrone has joined.
07:47:58 -!- idris-bot has joined.
07:53:57 -!- Melvar` has changed nick to Melvar.
08:31:58 -!- Patashu has joined.
08:37:13 -!- Patashu_ has joined.
08:37:13 -!- Patashu has quit (Disconnected by services).
08:38:15 -!- Patashu_ has quit (Client Quit).
08:38:29 -!- Patashu has joined.
08:41:42 -!- Patashu has quit (Disconnected by services).
08:41:42 -!- Patashu_ has joined.
08:58:24 -!- Phantom_Hoover has joined.
09:14:21 <Taneb> `quote bad pr
09:14:22 <HackEgo> 193) <elliott> Getting bad programmers to like something is a failure.
09:14:27 <Taneb> `quote bad pr to
09:14:28 <HackEgo> No output.
09:14:33 <Taneb> `quote experimenting
09:14:34 <HackEgo> 434) <Taneb> Well, I'm now experimenting with clients <fizzie> It doesn't sound like good PR to say that out loud.
09:14:45 <Taneb> Help I'm using IRSSI again
09:15:13 <fizzie> You just can't stop, can you.
09:16:31 <Taneb> Also I'm reading bad PHP, too
09:39:28 <Taneb> Also, new version of Dwarf Fortress aaaaaaah
09:39:45 <myname> wooooot
09:40:15 <myname> woah
10:10:19 <Phantom_Hoover> sadly dfhack won't be updated forever
10:10:21 -!- boily has joined.
10:12:37 <Taneb> Phantom_Hoover: will your Anthracite mod be updated?
10:13:13 <Phantom_Hoover> p. sure it already is, he won't have changed the stone system
10:15:30 <Taneb> You may have to send it to me again in a couple of weeks
10:16:41 <Phantom_Hoover> i'm not sure i even have a copy any more
10:16:55 <Phantom_Hoover> you can make your own very easily though!
10:19:27 <elliott> we should do a succession fort again
10:24:24 <Phantom_Hoover> yesss
10:24:40 <Phantom_Hoover> meanwhile i'm in #dfhack and
10:24:41 <Phantom_Hoover> <Sparts> I think walls are completely unusable in new version fort mode
10:24:46 <Phantom_Hoover> <Sparts> Apparently when you deconstruct one everything in your fort teleports near the deconstructed spot
10:24:53 <Sgeo> We should learn to fix Sgeo's sleep patterns so that when coworkers randomly call in the dead of night he's actually woken up
10:24:56 <Phantom_Hoover> the potential for abuse is real
10:49:52 -!- yorick has joined.
10:55:35 -!- Patashu has joined.
10:56:58 -!- Patashu_ has quit (Ping timeout: 240 seconds).
10:57:39 -!- idris-bot has quit (Quit: Terminated).
10:57:55 -!- idris-bot has joined.
10:58:10 -!- idris-bot has quit (Client Quit).
11:02:19 -!- idris-bot has joined.
11:10:30 -!- boily has quit (Quit: SCRAMBLED CHICKEN).
11:14:08 <Melvar> ( :let nats : Stream Nat; nats = iterate S Z
11:14:08 <idris-bot> defined
11:14:25 <Melvar> ( take 10 nats
11:14:25 <idris-bot> [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] : Vect 10 Nat
11:15:33 -!- shikhin has joined.
11:18:43 <elliott> @ask ais523 do we actually want that infobox?
11:18:43 <lambdabot> Consider it noted.
11:41:30 <Taneb> elliott: which infobox?
11:42:01 <elliott> the one germanyboy made on the wiki
11:47:34 <Melvar> `` units '2 pounds * c^2' 'megatons tnt'
11:47:35 <HackEgo> ​* 19.487022 \ / 0.051316205
11:51:50 -!- shikhout has joined.
11:55:11 -!- shikhin has quit (Ping timeout: 264 seconds).
11:55:13 * Melvar finds out that in units, “lightyear” is not the same as “light year”, because “lightyear” is “c * julianyear” but “year” defaults to “tropicalyear”.
12:04:14 <Phantom_Hoover> for some reason df2014 has thrown my keyboard bindings into a blender
12:06:34 <Phantom_Hoover> worldgen is way more dynamic and way, waaaay slower
12:06:53 <elliott> that's why it only runs for two weeks or something, right?
12:07:02 <Phantom_Hoover> that's between forts
12:07:14 <Phantom_Hoover> the initial worldgen is still 256 years by default
12:07:40 <Phantom_Hoover> i assume it's a coarser simulation than the fort-to-fort one though
12:18:41 <Phantom_Hoover> it also crashed at the end of worldgen
12:20:22 -!- nooodl has joined.
12:23:17 <fizzie> IDGI. Images from the phone become more blurry if I shorten the exposure time.
12:23:57 -!- MindlessDrone has quit (Quit: MindlessDrone).
12:24:48 <fizzie> `run units '1 light year' 'lightyears'
12:24:58 <HackEgo> ​* 0.99997864 \ / 1.0000214
12:25:02 <fizzie> Fancy.
12:25:26 -!- Sorella has joined.
12:28:42 <Melvar> `` units lightyear; units year
12:28:42 <HackEgo> ​Definition: c julianyear = 9.4607305e+15 m \ Definition: tropicalyear = 365.242198781 day = 31556926 s
12:42:52 -!- vifino has joined.
12:51:17 <ion> `run units 'light ray'
12:51:17 <HackEgo> ​Definition: 2.9979246e+13 kg / m^3 s^2
12:53:16 <Melvar> Ooh, I specified “beard” in my .units, that’s why it’s not there. Derp.
12:53:19 <ion> `run units 'bu bbl e'
12:53:19 <HackEgo> ​Definition: 8.976297e-22 A m^6 s
12:53:55 <Melvar> `units smoot
12:53:55 <HackEgo> ​Definition: 5 ft + 7 in = 1.7018 m
12:55:37 <ion> Hah, the story behind that is funny.
12:56:55 <ion> Especially given his current job.
12:57:17 <ion> s/current/last/
13:01:19 <Melvar> `` units 'light nanosecond' 'feet'
13:01:20 <HackEgo> ​* 0.98357106 \ / 1.0167034
13:02:50 <fizzie> `units sheppey
13:02:51 <HackEgo> Unknown unit 'sheppey'
13:02:53 <fizzie> Aw.
13:03:57 <Melvar> http://en.wikipedia.org/wiki/List_of_unusual_units_of_measurement
13:05:48 <int-e> `units shed
13:05:48 <HackEgo> ​Definition: 1e-24 barn = 1e-52 m^2
13:12:27 <Melvar> `units billion
13:12:28 <HackEgo> ​Definition: shortbillion = 1e9 = 1e+09
13:12:34 <Melvar> `units longbillion
13:12:35 <HackEgo> ​Definition: million^2 = 1e+12
13:14:38 <Melvar> `units gram
13:14:39 <HackEgo> ​Definition: millikg = 1e-3 kg = 0.001 kg
13:16:08 <Melvar> ↑ lol @ millikg. But correct, since the kilogram is the base unit as defined in the SI.
13:16:46 <ion> :-)
13:17:28 <Melvar> IIRC it’s also the only one still defined by a prototype.
13:18:00 <fizzie> Yes, though they keep trying to get rid of that.
13:18:02 <Melvar> Which turns out to be a problem, since the prototype and its copies have been drifting relative to one another, as we can now measure.
13:21:24 <Melvar> `` units 'pi seconds' nanocentury
13:21:25 <HackEgo> ​* 0.9955319 \ / 1.0044882
13:22:17 <ion> nice
14:03:04 -!- tswett has joined.
14:03:39 <tswett> Ahoy.
14:08:20 -!- Patashu has quit (Ping timeout: 240 seconds).
14:10:17 <tswett> So I decided to come up with an esolang that's pretty much an assembly language with a static, strong, and extremely flexible type system.
14:11:03 -!- Speed` has quit (Ping timeout: 240 seconds).
14:11:25 <tswett> This turns out to be really complicated.
14:11:28 -!- HoverZuu has changed nick to Zuu.
14:13:54 -!- Speed` has joined.
14:16:37 <b_jonas> tswett: do you mean an assembly language where the output maps directly to some existing machine code, but the assembly language itself restricted by a type system so that it can find some errors and make programming easier?
14:17:16 <b_jonas> tswett: because that language almost exists, it's C
14:17:51 <b_jonas> except that C can copy structures by value
14:18:11 <tswett> Vaguely like C, except that it would be lower level, and the type system would be much more flexiblestrong.
14:18:46 <tswett> Like, consider a "dup" instruction, which duplicates the top word on the stack.
14:19:42 <tswett> This instruction would have the type "piece of code starting with a stack containing some initial stuff, then a word of type 'a', then some blank space, and ending with the original stuff, then two words of type 'a', then one word less blank space".
14:21:07 <tswett> Or something like "forall (i :: Mem) (a :: Word) (n :: Nat), i ** a ** (n + 1) Blank -> i ** a ** a ** n Blank"
14:21:37 <Melvar> Sounds like the sort of thing you’d do as an embedded DSL in Idris.
14:22:27 <tswett> Melvar: yup.
14:52:14 <tswett> I'll start by making the "little" version of the language. It'll make some simplifying assumptions, like that the stack has infinite room to grow.
14:53:12 <tswett> And that a word can store an entire arbitrary-precision natural number.
15:00:15 -!- Sgeo has quit (Read error: Connection reset by peer).
15:36:34 -!- ajf has joined.
15:36:42 <ajf> So
15:36:58 <ajf> In Bash and some other languages, “fi” (“if” backwards) ends an if statement
15:37:06 <ajf> But I think it doesn’t have enough context
15:37:11 <ajf> So how about this?
15:37:16 <ajf> if (x == 3)
15:37:20 <ajf> fi x) == )3
15:37:27 <ajf> Or, for example
15:37:33 <ajf> if (foobar == qux)
15:37:44 <ajf> fi raboof( == )xuq
15:38:04 <ajf> I’ve got to use this in my next esoteric language ^^
15:38:56 -!- shikhout has changed nick to shikhin.
15:49:23 <Bike> syntactic rules unclear. better to use the negation. if (x == 3) fi (x != 3)
15:52:51 -!- drdanmaku has joined.
15:53:19 <ajf> Bike: Ah, yes
15:53:33 <ajf> Also, it would intelligently understand english
15:53:34 <ajf> For example
15:53:46 <ajf> if (thing.delete(3))
15:53:53 <ajf> fi (thing.create(3))
15:53:57 -!- edwardk has quit (Quit: Computer has gone to sleep.).
15:54:39 <ajf> Or maybe just prepend un
15:54:47 <ajf> if (thing.delete(foo))
15:54:52 <ajf> fi (unthing.undelete(unfoo))
15:55:01 <ajf> Similarly:
15:55:06 <ajf> if (unthing.undelete(unfoo))
15:55:16 <ajf> fi (ununthing.unundelete(ununfoo))
16:02:22 -!- oerjan has joined.
16:07:12 -!- shikhin has quit (Ping timeout: 240 seconds).
16:07:31 -!- shikhin has joined.
16:11:44 -!- d00p_ has joined.
16:13:18 -!- ais523 has joined.
16:14:57 <ais523> oh well, patch-tag just admitted that it isn't up any more
16:15:04 <ais523> but it did so via email with all its users in the To: field
16:15:15 <ais523> I wonder how many people will complain about that
16:15:56 -!- AnotherTest has quit (Ping timeout: 240 seconds).
16:16:01 <ais523> ooh, someone complained via reply-all :-)
16:16:28 <ais523> if Raymond Chen's blog has taught me anything, it's that we're only 2 or 3 messages away from going exponential
16:17:42 <ais523> meanwhile, I discovered something in my research recently, and am wondering whether it's new (I hope it isn't, because it's confusing to think about and I'm hoping someone will have done the hard part already)
16:18:20 <int-e> ais523: classic
16:18:28 <int-e> ais523: any out of office replies?
16:18:30 <ais523> when you have a type like "a -> b -> a", that's shorthand for "forall a, b.a -> b -> a"
16:18:37 <ais523> int-e: not reply-all'ed
16:18:41 <int-e> pity ;)
16:18:56 <ais523> I've come across a type of the form "forall a.exists b.a -> b -> a"
16:19:01 <ais523> and want to know if anyone's ever seen anything like that before
16:19:07 <int-e> (imagine two reply-all out of office replies playing ping pong)
16:19:15 <ais523> surely it's got to exist as some obscure GHC feature or something
16:19:39 <b_jonas> ais523: it does exist as a very useful ghc extension, yes
16:19:45 <ais523> oh good
16:19:48 <b_jonas> and has some surprising applications too
16:19:51 <ais523> are there any academic papers about it?
16:19:54 <b_jonas> you'd better ask on #haskell
16:19:56 <b_jonas> they'll help
16:20:24 <b_jonas> I'm not sure what it's called, maybe higher-order types?
16:20:26 <int-e> 'exists'? hmm.
16:20:59 <ais523> b_jonas: no, a higher-order type is one in which a function is used as an argument to another function
16:21:01 <ais523> as in (a -> b) -> a
16:21:18 <b_jonas> higher-rank type sorry
16:21:55 <ais523> that's types of the form (forall a.a -> a) -> b
16:22:00 <int-e> ghc limits itself to 'forall' though.
16:22:03 <ais523> where the forall is inside parens rather than on the outside
16:22:16 <b_jonas> isn't that like equivalent though?
16:22:28 <b_jonas> don't you get exists free from foreach or from gadt or something?
16:22:38 <ais523> I very much hope so
16:24:03 <b_jonas> this is about the syntax of the extension in ghc: http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/data-type-extensions.html#existential-quantification
16:24:25 <b_jonas> though you may have to read it together with other extensions like gadt and stuff
16:24:32 <b_jonas> but as for the applications, better ask #haskell
16:26:43 <oerjan> gadt's include existentials as a subfeature
16:26:46 -!- ais523_ has joined.
16:26:59 <oerjan> <oerjan> gadt's include existentials as a subfeature
16:28:32 <int-e> I guess forall a.exists b. a -> b -> a === forall a r.(forall b. (a -> b -> a) -> r) -> r
16:28:48 <ais523_> right, but now the type has a different shape
16:28:52 <oerjan> b_jonas: ghc uses forall in some positions to denote existentials, essentially by demorgan duality
16:29:03 <ais523_> but yes, I was coming to that conclusion myself
16:29:22 -!- ais523 has quit (Ping timeout: 245 seconds).
16:29:23 <ais523_> the (f === (f -> r) -> r) equivalence is often useful in practice for notating types that would otherwise be un-notatable
16:29:50 <oerjan> data YourType a where MyConstructor :: (a -> b -> a) -> YourType a
16:30:12 <oerjan> i think that's gadt for exists b. (a -> b -> a)
16:30:14 <int-e> existential datatypes are based on the same trick; if you look at a constructor, you get things like Foo :: forall b. b -> Foo
16:31:08 <oerjan> or without gadt's, data YourType a = forall b. MyConstructor (a -> b -> a)
16:31:18 <oerjan> *without gadt syntax
16:32:15 <int-e> so how is this useful? the only thing I can ever imagine passing for the argument of type 'b' is 'undefined'.
16:32:27 <oerjan> i don't see how this particular type is useful
16:32:40 <oerjan> since you can indeed never know what to pass to it
16:33:02 <ais523_> well, I don't think I've explained the situation very well
16:33:22 <ais523_> the actual case I have is a function which, given the type of its return value, constructs matching types for the two arguments
16:33:33 <ais523_> however, it doesn't always do so the same way
16:33:54 <b_jonas> ais523_: I really recommend you to ask on #haskell
16:34:05 <ais523_> this is too esoteric for #haskell :-)
16:34:05 -!- ais523 has joined.
16:34:13 <int-e> ais523: it's not
16:34:25 <ais523_> I don't think it works in Haskell because such a function necessarily has to be impure
16:34:34 <b_jonas> too esoteric for #haskell ? no way!
16:35:04 <ais523_> I need to work out exactly how it is that this type behaves, at least
16:35:34 <int-e> a function of type Foo a => a -> exists b. (b, a -> b -> a) could make perfect sense
16:35:34 <ais523_> so, the situation is, I have a type that represents a value that's only valid for a particular, abstract, period of time
16:35:53 <ais523_> and the main operation that makes sense on these periods is taking the union
16:35:54 <int-e> (note the type class, so that it can do different things depending on the type of a.)
16:35:54 <b_jonas> ais523_: like the thingies in ST?
16:35:58 <oerjan> ais523_: i think what you mean is that your function must be non-parametric
16:36:12 <oerjan> you have to be able to distinguish types.
16:36:27 <oerjan> also, come to think of it, there clearly is a value of that type: const
16:36:34 <ais523_> so, e.g., the type of sequential composition (i.e. "do a then b" is t1.command -> t2.command -> (t1 + t2).command)
16:36:45 <oerjan> it just happens to have the type forall a b. a -> b -> a, which is stronger.
16:36:54 <ais523_> except, if I have two sequential compositions that both return a (t1 + t2).command
16:36:56 <int-e> @type flip seq
16:36:57 <lambdabot> c -> a -> c
16:37:02 <ais523_> they might need different t1s and t2s
16:37:15 <ais523_> because we can't guarantee that the first argument to each will end at the exact same time
16:37:16 <int-e> (I know, seq is just const's evil twin)
16:37:53 <b_jonas> ais523_: dunno, still sounds sort of like ST
16:38:07 <ais523_> it's basically just a mess
16:38:30 <ais523_> it seems to be the same sort of category as a name generator function, just on types, rather than values
16:38:39 <int-e> ais523: sounds like 'unamb' here: http://hackage.haskell.org/package/unamb-0.2.5/docs/Data-Unamb.html
16:38:49 <b_jonas> no, it sounds like ST
16:39:03 <ais523_> (what a name generator function does is, everytime you call it, it returns a different value; the only meaningful operation you can do on such values is compare them to themselves (equal), and compare them to each other (unequal))
16:39:16 <int-e> oerjan is probably right ;)
16:39:36 <ais523_> "non-parametric" is a good word for this sort of thing, yes
16:39:41 <ais523_> or rather, it's coparametric
16:40:01 <ais523_> instead of working on multiple types, determined by the context
16:40:07 <int-e> oleg has some stuff on monadic regions
16:40:10 <ais523_> it determines which types the context must have
16:40:38 <b_jonas> still sounds like ST magic
16:40:40 <int-e> which may also be relevant.
16:40:47 <b_jonas> (magic in the positive sense)
16:40:49 <ais523_> oh wow, Google only has 10 results for "coparametric", all of which are irrelevant
16:41:33 -!- lollo64it has joined.
16:42:12 <b_jonas> ais523_: read up on how ST works, or ask #haskell how it works, because I think you want somethign close to that
16:42:15 <oerjan> we need to get copumpkin and edwardk to invent something relevant
16:42:58 <Melvar> ( :doc Exists
16:42:58 <idris-bot> Data type Exists : (P : a -> Type) -> Type
16:42:58 <idris-bot> Dependent pair where the first field is erased.
16:42:58 <idris-bot> Constructors:
16:42:58 <idris-bot> evidence : (x : a) -> (pf : P x) -> Exists P
16:43:03 <b_jonas> or ask #haskell where to read up on it
16:44:22 <Melvar> ( (a : Type) -> Exists (\b => a -> b -> a)
16:44:22 <idris-bot> (a : Type) -> Exists (\b => a -> b -> a) : Type
16:44:25 <int-e> from Control.Monad.ST: "This library provides support for strict state threads, as described in the PLDI '94 paper by John Launchbury and Simon Peyton Jones Lazy Functional State Threads."
16:45:59 <ais523_> this isn't much to do with ST, I don't think
16:46:31 <b_jonas> can you tell why?
16:46:36 <Melvar> You can produce a value of this type, but you can’t do anything with it because pattern matching on types is forbidden.
16:47:28 <ais523_> b_jonas: because ST is a monad which has run-time behaviour
16:47:38 <ais523_> and this is all at the type system level
16:47:57 <oerjan> just apply datakinds
16:48:00 <ais523_> Melvar: are there any applications of Idris' Exists?
16:48:49 <b_jonas> ais523_: but I mean the type system magic part of ST
16:48:56 <Melvar> ( the (Exists (\n => Vect n Integer)) $ evidence _ [1,2,3]
16:48:56 <idris-bot> evidence 3 [1, 2, 3] : Exists (\n => Vect n Integer)
16:49:06 <b_jonas> ST stuff have a type too, not only runtime behaviour
16:49:08 <Melvar> ( the (Exists (\n => Vect n Integer)) $ evidence _ [1,2,3,4,5]
16:49:08 <idris-bot> evidence 5 [1, 2, 3, 4, 5] : Exists (\n => Vect n Integer)
16:49:37 <int-e> @type Control.Monad.ST.runST
16:49:38 <lambdabot> (forall s. ST s a) -> a
16:50:22 <ais523_> in my case, I want other functions to be able to generate values of the hidden types, but only by being parametric on them
16:50:24 <Melvar> You can use it to allow any value for some index of a type.
16:50:27 <int-e> @type Data.STRef.newSTRef
16:50:27 <olsner> was the point in the original "forall a. exists b. a -> b -> a" that b depends on a in some special way?
16:50:28 <lambdabot> a -> ST s (STRef s a)
16:50:28 <ais523_> and then I have to bundle all this into a type system somehow
16:50:47 <ais523_> Melvar: is the _ being inferred somehow?
16:51:11 <Melvar> ais523_: _ means “fill this in by unification”.
16:51:13 <int-e> (that's pretty much the whole magic: the "STRef" has a phantom type parameter 's' that binds it to a particular call of 'runST')
16:51:14 <b_jonas> @type Control.Monad.ST.runST
16:51:15 <lambdabot> (forall s. ST s a) -> a
16:52:31 <olsner> if so, maybe a type family or a type class with an associated type or fundeps could do it?
16:54:06 <Melvar> ais523_: The thing is that [1,2,3] is definitely a (Vect 3 Integer), and unification with the type of evidence thus determines what its first argument must be.
16:54:25 <ais523_> right, yes
16:54:55 <ais523_> most of the work is done by evidence, rather than Exists, it seems; but you can only create an Exists using an evidence
16:54:57 <ais523_> so that doesn't really matter
16:55:17 <Melvar> ?
16:55:32 <Melvar> I don’t really see how the two are extricable.
16:57:16 <Melvar> Also, with Exists the first value is erased, i.e. the compiler will do its best to make it not exist at runtime.
16:57:51 <Melvar> Which corresponds to one of the three interpretations of a dependent pair, the other two corresponding to Sigma and Subset.
16:57:59 <Melvar> ( :doc Sigma
16:57:59 <idris-bot> Data type Sigma : (a : Type) -> (P : a -> Type) -> Type
16:57:59 <idris-bot> Dependent pairs, in their internal representation
16:57:59 <idris-bot> Arguments:
16:57:59 <idris-bot> a : Type -- the type of the witness
16:57:59 <idris-bot> P : a -> Type -- the type of the proof↵…
16:58:11 <Melvar> ( :doc Subset
16:58:11 <idris-bot> Data type Subset : (a : Type) -> (P : a -> Type) -> Type
16:58:11 <idris-bot> Dependent pair where the second field is erased.
16:58:11 <idris-bot> Constructors:
16:58:11 <idris-bot> element : (x : a) -> (pf : P x) -> Subset a P
16:58:54 <ais523_> anyway, I now know to not try to write this explanation in terms of exists, because it's just subtly different enough from the usual meaning that it'd confuse people
17:01:55 <ais523_> "copolymorphism" is a good definition of what's going on here, and has 1 Google hit, which is irrelevant
17:04:50 <tswett> This sounds complicated.
17:06:28 <ais523> I'm not surprised that I've been stuck on it for months
17:06:53 -!- shikhout has joined.
17:07:43 <tswett> Like my attempts to write linear logic types as Haskell types.
17:08:00 <oerjan> you're just doing things man was not meant to know hth
17:08:03 -!- shikhin has quit (Ping timeout: 240 seconds).
17:09:15 <tswett> Of course, it doesn't really make sense to simply write a linear logic type as a Haskell type, because the very existence of a Haskell type for an object implies that you can do things you may not be able to do with a linear object.
17:10:31 <tswett> Like, an LL function "(a * a) -o (a * a)" isn't a Haskell function "(a, a) -> (a, a)", because the LL function must be called exactly once, and the Haskell type doesn't express that restriction.
17:10:56 <tswett> Indeed, linear objects can't actually exist in Haskell, at least not as Haskell objects.
17:11:40 <tswett> The things that *can* exist are Haskell objects that happen to somehow implement LL objects.
17:12:36 <tswett> So, we might say that the Haskell type "Pf A" denotes a Haskell object that can be used as an LL object whose type is A.
17:14:05 <Melvar> tswett: By “-o”, did you mean “⊸”?
17:14:10 <tswett> Melvar: yes.
17:14:25 <tswett> The problem is, Pf doesn't distribute. (Or factor through or whatever).
17:14:41 <tswett> You can't write Pf (A -o B) in terms of Pf A and Pf B.
17:15:07 -!- shikhout has changed nick to shikhin.
17:15:20 <tswett> Pf Zero and Pf Bottom are both the same thing (the empty type), because there are no Haskell objects which behave as either a Zero or a Bottom.
17:16:40 -!- edwardk has joined.
17:16:58 <tswett> However, while Pf (Zero -o Bottom), Pf (Zero -o Zero), and Pf (Bottom -o Bottom) all exist (they're exfalso, exfalso, and id, respectively), Pf (Bottom -o Zero) doesn't exist.
17:17:20 -!- MoALTz has joined.
17:32:37 -!- `^_^v has quit (Ping timeout: 248 seconds).
17:32:49 -!- Phantom_Hoover has quit (Remote host closed the connection).
17:34:31 -!- Phantom_Hoover has joined.
17:41:02 -!- shikhin has quit (Ping timeout: 245 seconds).
18:04:33 <tswett> Hmm. Using | to represent the par operator, those are Pf (Top | Bottom), Pf (Top | Zero), Pf (One | Bottom), and Pf (One | Zero). Might be easier to think about, I dunno.
18:05:11 <tswett> Pf Top and Pf One both exist. Pf (Top | Zero) exists, but Pf (One | Zero) doesn't.
18:06:50 <tswett> This is because an object obeying the Top protocol can keep making requests forever, so in order to obey the Top | Zero protocol (which requires you to obey both protocols in the order of your choice), you can just make requests forever.
18:07:33 <tswett> But an object obeying the One protocol just sits there and does nothing. In order to obey the One | Zero protocol, you have to obey both protocols in the order of your choice. You can obey the One protocol, but then that protocol will terminate, and you'll have to obey the Zero protocol, which is impossible.
18:12:29 -!- `^_^v has joined.
18:25:31 -!- `^_^v has quit (Quit: This computer has gone to sleep).
18:27:50 -!- `^_^v has joined.
18:31:21 <HackEgo> [wiki] [[Ligature Machine]] http://esolangs.org/w/index.php?diff=40111&oldid=40107 * Zzo38 * (+449)
18:32:04 -!- edwardk has quit (Ping timeout: 240 seconds).
18:59:25 -!- AnotherTest has joined.
19:04:14 -!- Bicyclidine has joined.
19:18:47 -!- tswett has quit (Quit: tswett).
19:26:07 -!- edwardk has joined.
19:39:18 -!- edwardk has quit (Quit: Computer has gone to sleep.).
19:46:04 -!- edwardk has joined.
19:50:16 -!- MindlessDrone has joined.
19:53:10 -!- `^_^v has quit (Quit: This computer has gone to sleep).
19:53:28 -!- `^_^v has joined.
19:58:18 -!- lollo64it has quit (Ping timeout: 240 seconds).
20:23:35 -!- edwardk has quit (Quit: Computer has gone to sleep.).
20:27:58 -!- edwardk has joined.
20:38:52 -!- `^_^v has quit (Quit: This computer has gone to sleep).
20:39:40 -!- `^_^v has joined.
20:42:42 -!- MindlessDrone has quit (Quit: MindlessDrone).
20:42:48 -!- nycs has joined.
20:45:37 -!- `^_^v has quit (Ping timeout: 245 seconds).
20:53:55 -!- tswett has joined.
20:53:57 -!- AnotherTest has quit (Ping timeout: 245 seconds).
20:54:09 <tswett> So, what's the best unusable esolang?
20:54:33 <Bicyclidine> Most ever Brainfuckiest Fuck you Brain fucker Fuck
20:55:18 <tswett> http://esolangs.org/wiki/Minimum – I like this one.
20:55:33 <tswett> The language's syntax:
20:55:42 <tswett> <program> ::= "`" <program> <program>
20:56:28 <nooodl> i like http://esolangs.org/wiki/Subtle_cough
20:56:39 <nooodl> i guess minimum is the EXTREME version of subtle cough
20:57:35 <ais523> at least, in Subtle Cough, it looks vaguely like it might be TC, but it isn't
20:57:59 <ais523> in Minimum, it's hard to even write the program (there is only one program), and it's also hard to figure out what it is that that program does
20:58:57 <tswett> There's only a program if you interpret the syntax coinductively instead of inductively.
20:59:05 <Bicyclidine> > repeat '`'
20:59:07 <lambdabot> "```````````````````````````````````````````````````````````````````````````...
20:59:24 <Bicyclidine> in my scientific opinion the program does bupkis
20:59:27 <tswett> And evaluation of Unlambdoids is defined inductively, not coinductively.
21:01:39 -!- tromp has joined.
21:03:02 <oerjan> just do it lazy, 'k
21:06:39 <tswett> All right. Language:
21:07:53 <tswett> A program consists of a sequence of digits. Execution consists of repeatedly selecting an unspecified pair of identical digits, and replacing the digits and everything between them with a number of copies of the stuff in between them equal to that digit.
21:08:07 <tswett> So, like, the program 51235 becomes 123123123123123.
21:08:22 <tswett> And then that program probably explodes or something.
21:08:41 <ais523> tswett: reminds me of XigXag
21:08:47 <Bicyclidine> i don't think this is as suitable to bicyclidal enterprises as Most ever Brainfuckiest Fuck you Brain fucker Fuck is
21:08:50 <tswett> Yup.
21:08:58 <ais523> which is currently along with Dupdog in the "we're sure this isn't TC but can't quite articulate why" category
21:09:26 <ais523> tswett: aren't all 1s completely irrelevant in that language?
21:09:30 <ais523> you could do interesting things with 0s, though
21:09:36 <tswett> I guess they are, yeah.
21:09:48 <tswett> The only thing 1s ever do is vanish.
21:10:13 <tswett> (Also, SLOBOL needs to be replaced.)
21:10:36 <tswett> Ooh. Ooh. We need a language based on diffusion-limited aggregation.
21:10:43 <elliott> tswett: not true
21:10:51 <elliott> 2123
21:10:57 <elliott> can become 113 can become 33333333333
21:11:32 <ais523> elliott: no, 113 can only become 3
21:11:41 -!- conehead has quit (Read error: Connection reset by peer).
21:12:02 <elliott> oh, right
21:12:08 <elliott> I was thinking look-and-say
21:21:15 -!- conehead has joined.
21:24:15 <nooodl> "<ais523> [...] it's also hard to figure out what it is that that program does" <- i guess it just does nothing and never terminates?
21:24:43 <ais523> nooodl: you go into an infinite regress trying to work out what happens first
21:25:57 <Bicyclidine> common problem
21:29:48 -!- callforjudgement has joined.
21:30:05 -!- ais523 has quit.
21:30:54 -!- callforjudgement has changed nick to ais523.
21:31:42 -!- Bike has quit (Ping timeout: 240 seconds).
21:33:42 -!- Bike has joined.
21:37:12 -!- ais523 has quit (Ping timeout: 240 seconds).
21:45:05 -!- edwardk has quit (Quit: Computer has gone to sleep.).
21:45:24 -!- oerjan has quit (Quit: leaving).
22:06:57 -!- boily has joined.
22:07:52 -!- metasepia has joined.
22:08:40 <boily> 27m34s! WOOHOO!
22:11:56 <nooodl> boily: ?
22:14:00 <boily> when you're subscribed to Bixi you get a log of all time you use a bike, with end stations and the time it took.
22:14:14 <boily> s/time y/times y/
22:14:25 <boily> (or something ungrammatical like that)
22:14:54 <boily> the trajet back home from work is uphill, with uphill slopes that go up.
22:14:59 <boily> tonight I broke my record! :D
22:17:52 <FireFly> Congrats
22:21:49 <FireFly> tswett: is this numbers thing on the wiki?
22:26:33 -!- Bike has quit (Ping timeout: 240 seconds).
22:28:46 -!- Bike has joined.
22:36:19 -!- nooodl_ has joined.
22:39:08 -!- nooodl has quit (Ping timeout: 240 seconds).
22:40:00 -!- edwardk has joined.
22:48:24 <tswett> FireFly: no, it isn't.
22:49:11 <tswett> Stupid programming language:
22:49:24 <tswett> There are four commands: n, e, s, and w.
22:49:51 <boily> e
22:50:05 <Bicyclidine> > inventory
22:50:05 <tswett> The state is a point in space.
22:50:06 <lambdabot> Not in scope: ‘inventory’
22:50:18 <tswett> The point is initially (0, 0, 1).
22:50:45 <tswett> n rotates the point one radian clockwise about the x-axis as seen from the positive direction.
22:51:06 <tswett> e rotates the point one radian counterclockwise about the y-axis as seen from the positive direction.
22:51:10 <tswett> s undoes n. w undoes e.
22:53:19 <ais523_> any sort of conditional branch?
22:53:34 <ais523_> if there is, I wouldn't be able to say definitively that it isn't TC
22:53:44 <tswett> Ooh.
22:53:45 <tswett> Ooh.
22:53:50 <tswett> Okay.
22:53:59 <ais523_> at least, not without more thought
22:54:02 <tswett> Parentheses mean "loop while z > 0".
22:54:12 <ais523_> yay
22:54:13 <tswett> Now is it Turing-complete?
22:54:18 <ais523_> I don't know
22:54:25 <boily> what can it compute?
22:54:28 <ais523_> it doesn't fail any of the checks that make a language obviously Turing-incomplete
22:54:41 <FireFly> Wouln't a (non-looping) conditional suffice if a looping one does?
22:54:41 <ais523_> when failed
22:54:50 <ais523_> FireFly: no, because then the program always halts
22:55:14 <FireFly> I mean, you could get loopedness by applying one of the rotation commands sufficiently
22:55:24 <FireFly> wait
22:55:33 <FireFly> never mind
22:55:41 <ais523_> you're confusing loops in the program with loops in the data
22:56:11 <FireFly> I see that now
22:56:25 <tswett> In theory, you can store an arbitrary amount of data here.
22:56:39 <tswett> Like, you can sort of use the point as two registers storing integers up to a certain limit.
22:56:47 <tswett> Increment and decrement the integers using tiny rotations.
22:57:02 <tswett> But the two registers interfere with each other.
22:57:46 <tswett> Also, instructions are written from right to left, just for the hell.
22:57:56 -!- Phantom_Hoover has quit (Ping timeout: 240 seconds).
22:58:54 <boily> tswett: itym “just for the AP-heLL”
22:59:03 <tswett> What's AP-heLL?
23:00:21 <boily> bad pun, poorly written. you said that it's written RTL, just like APL.
23:00:33 * boily mapoles himself a few times in penance
23:00:37 <tswett> Mm.
23:01:53 -!- Sgeo has joined.
23:03:46 <tswett> This company I want to work for asks me to "show me some interesting code you've written and walk me through it". I'm trying to think if I've really written any interesting code.
23:04:39 <tswett> Nah, I'm sure I have.
23:06:19 <tswett> Here's something called FPS.hs. I can't remember what it is at all.
23:06:36 <Bicyclidine> estimates the frames per second for an attached process running Quake
23:06:42 <tswett> (FPS xs) * (FPS ys) = FPS . map (sum . map (uncurry (*))) . tail $ convolute xs ys
23:06:45 <tswett> Bicyclidine: probably.
23:08:09 <Melvar> What does convolute do?
23:08:25 <boily> it does a convolution, duh :P
23:08:53 <tswett> convolute :: [a] -> [b] -> [[(a,b)]]
23:09:21 <tswett> That's not quite convolution actually is.
23:09:37 <Bicyclidine> lol.
23:09:40 <boily> I expected convolute :: [a] -> [a] -> [a].
23:09:52 <Bicyclidine> well, that's why tswett is walking you through it, now isn't it
23:11:54 * tswett looks through his code.
23:13:36 <tswett> In my Docs/Programming directory, I have an HTML directory.
23:13:51 <tswett> I looked in there expecting to find some cute Javascript things.
23:14:12 <tswett> Turns out that the only thing in there is a single HTML file. And sure enough, it's pure HTML, with no Javascript at all.
23:14:30 <tswett> Well, I guess half of it is CSS.
23:15:12 <Bicyclidine> it's good to be organized.
23:17:29 <tswett> Sweet. I have my implementation of Subleq in Verilog.
23:18:10 <subleq> I am _not_ in Verilog
23:18:26 <tswett> Oh yeah? Explain this!
23:18:29 <ais523_> convolution doesn't necessarily apply only to lists, but it requires some sort of sum
23:19:03 <Bicyclidine> discrete schmiscrete
23:19:06 <tswett> Summing is appending.
23:19:11 <tswett> subleq: https://clbin.com/VZNL5
23:19:15 <ais523_> I think the definition is "convolute f g x = sum (d from -infinity to infinity) of f(x-d) * g(d)"
23:19:38 <ais523_> for any appropriate definitions of -, *, sum you can think of
23:20:13 <Bicyclidine> probably you can use something other than the reals to sum over, too
23:20:50 <Bicyclidine> yeah looks like there's a simple extension to higher dimensions, for a start
23:21:07 <ais523_> err yes, I should probably rephrase it like this
23:21:29 <ais523_> "convolute f g x = sum (all y, z st y + z = x) f(y) * g(z)"
23:22:00 <elliott> this seems a bit...........................................................
23:22:02 <elliott> convoluted
23:22:16 <ais523_> convolution isn't a very simple operation
23:22:33 <Bicyclidine> psh it's just a product on the space of functions
23:22:52 <Bicyclidine> functions on arbitrary groups as long as they're measurable, looks like
23:23:01 <Bicyclidine> http://upload.wikimedia.org/math/f/5/3/f53180acc7806c4139550527dcaa6a13.png booyeah
23:24:03 <Bicyclidine> as for me, i'm just amused that convolve is the standard way to multiply polynomials in matlab.
23:24:23 * tswett ponders the convolution of polynomials.
23:24:48 <tswett> Of polynomial functions, not polynomial expressions.
23:27:39 <nooodl_> hm what's that λ
23:27:52 <Bicyclidine> the measure, i think.
23:28:04 <Sgeo> This is interesting: http://ddili.org/ders/d.en/ufcs.html
23:28:20 <Sgeo> Like extension methods except not required to explicitly be extension methods
23:28:20 -!- edwardk has quit (Quit: Computer has gone to sleep.).
23:28:39 <Sgeo> Removes temptation to make a method part of a class just for nicer syntax, I think.
23:29:29 <Bicyclidine> i just checked that the product of polynomials is not their convolution, because i'm an idiot i think
23:29:58 -!- edwardk has joined.
23:31:37 <tswett> You know, the hyperreal numbers are quite the thing.
23:32:43 <Sgeo> What about the hyporeal numbers?
23:33:11 <tswett> Hmmm.
23:33:14 <Bicyclidine> naturals?
23:33:35 <tswett> Nah, the hyporeal numbers are clearly the dyadic rationals.
23:33:51 <Bicyclidine> well, i guess you'd want a transfer principle.
23:34:09 <tswett> Hm, right.
23:34:50 <tswett> If the hyperreal numbers are an enlarged model of the real numbers (in some sense), then the hyporeal numbers must be a shrunk model.
23:34:58 <tswett> Maybe the hyporeal numbers are the definable numbers.
23:35:29 -!- edwardk has quit (Quit: Computer has gone to sleep.).
23:36:49 <Sgeo> Let alpha be the smallest positive non-definable number.
23:37:12 <tswett> But there's no such number.
23:37:25 <Bicyclidine> haha, that's a way better response than mine
23:38:15 <Sgeo> Right, because the definable numbers are just another way of saying 'interesting number' ;)
23:38:42 <Bicyclidine> no, because there isn't a smallest positive non-definable real any more than there's a smallest positive real
23:38:57 <Bicyclidine> of course, on top of that the defining language is something like first-order set theory that you can't recurse in.
23:39:03 <Bicyclidine> but tswett's answer is funnier.
23:39:16 <Sgeo> Bike: I know. (At least that first sentence)
23:40:24 <Bicyclidine> well i guess you could pick some weird fucking order, but fuck that
23:40:31 <tswett> (Consider alpha/2. Contradiction.)
23:40:36 <Bicyclidine> apparently there's a film called zorn's lemma? huh
23:40:55 <Sgeo> tswett: ... I assume that was a joke
23:40:56 <Bicyclidine> Zorns Lemma is a major poetic work. Created and put together by a very clear eye, this original and complex abstract work moves beyond the letters of the alphabet, beyond words and beyond Freud. If you don't understand it the first time you see it, don't despair, see it again! When you finally 'get it,' a small light, possibly a candle, will light itself inside your forehead.
23:41:09 <Sgeo> (In that my statement itself is inherently contradictory)
23:41:11 <Bicyclidine> we have entered an infinite recursion of humor
23:41:35 <Bicyclidine> this movie looks bad.
23:43:27 -!- vifino has quit (Quit: Ze Cat now leaves...).
23:53:29 -!- ais523 has joined.
23:57:50 -!- yorick has quit (Remote host closed the connection).
←2014-07-07 2014-07-08 2014-07-09→ ↑2014 ↑all