HNHacker News
TopNewBestAskShowJobs

psygnisfive

436 karma · joined September 1, 2007

Beka Valentine; trans dyke and general hacker bitch.
submissionscomments
psygnisfive··on Amazon is sticking ads in Prime Video shows and movies unless you pay more
ThePirateBay is not sticking ads in BitTorrented Video shows and movies no matter how little you pay
psygnisfive··on Help: FBI criminally charged me with $6MM loss for hotlinking. I didn't do it
Contact the Electronic Frontier Foundation. This is literally what they do. I don't know if they'll take up the case, but talk to them.
psygnisfive··on Welcoming Semmle to GitHub
> Security vulnerability finding is almost certainly the wrong target for Semmle

CVE-2019-5876

CVE-2019-16230

CVE-2019-16231

CVE-2019-16232

CVE-2019-16233

CVE-2019-16234

CVE-2019-15026

CVE-2019-14192

CVE-2019-14193

CVE-2019-14194

CVE-2019-14195

CVE-2019-14196

CVE-2019-14197

CVE-2019-14198

CVE-2019-14199

CVE-2019-14200

CVE-2019-14201

CVE-2019-14202

CVE-2019-14203

CVE-2019-14204

CVE-2019-14437

CVE-2019-14438

CVE-2019-14438

CVE-2019-14498

CVE-2019-14535

CVE-2019-14534

CVE-2019-14533

CVE-2019-14776

CVE-2019-14778

CVE-2019-14779

CVE-2019-14777

CVE-2019-14970

CVE-2019-15119

CVE-2019-14524

CVE-2019-14523

CVE-2019-7307

CVE-2019-11476

CVE-2019-13115

CVE-2019-3570

CVE-2019-13110

CVE-2019-13112

CVE-2019-13113

CVE-2019-13108

CVE-2019-13109

CVE-2019-13111

CVE-2019-13114

CVE-2019-3560

CVE-2019-9721

CVE-2019-9718

CVE-2019-9717

CVE-2019-9720

CVE-2019-9719

CVE-2018-20222

CVE-2019-3828

CVE-2019-6986

CVE-2019-5414

CVE-2018-4460

CVE-2018-16491

CVE-2018-16489

CVE-2018-16490

CVE-2018-19476

CVE-2018-19477

CVE-2018-19475

CVE-2018-19134

CVE-2018-16472

CVE-2018-18820

CVE-2018-4407

CVE-2018-16487

CVE-2018-4259

CVE-2018-4286

CVE-2018-4287

CVE-2018-4288

CVE-2018-4291

CVE-2019-5413

CVE-2018-16461

CVE-2018-16469

CVE-2018-16486

CVE-2018-16460

CVE-2018-16492

CVE-2018-11776

CVE-2018-8018

CVE-2018-8294

CVE-2018-4249

CVE-2018-8013

CVE-2018-5388

CVE-2018-1295

CVE-2018-4136

CVE-2018-4160

CVE-2018-1000140

CVE-2017-15692

CVE-2017-15693

CVE-2017-13904

CVE-2017-15089

CVE-2018-6834

CVE-2018-6835

CVE-2017-15713

CVE-2017-12634

CVE-2017-13782

CVE-2017-7545

CVE-2017-14949

CVE-2017-14868

CVE-2017-8046

CVE-2017-8045

CVE-2017-9805

CVE-2017-1000207

CVE-2017-1000208

CVE-2017-12612

CVE-2017-0141

https://lgtm.com/security/

psygnisfive··on So you want to write a type checker (2014)
mm.. perhaps I'm just not familiar enough with prolog, but I don't think it's possible to extract out a set of Prolog-level metavariables and compute over them? This is what's necesary to turn something like `_G947 -> _G947` into `forall a. a -> a`. but probably I just don't know enough. cool if you can, tho!
psygnisfive··on So you want to write a type checker (2014)
I'd also recommend Practical Foundations for Programming Languages (PFPL). And a bunch of other things, which I outlined here:

So You Want To Learn Type Theory (http://purelytheoretical.com/sywtltt.html)

psygnisfive··on So you want to write a type checker (2014)
Indeed! Tho this is only half the problem, because `T` there includes metavariables, so it's not a type but rather a schema at the meta-level for types. What we'd like is something like `forall a b c. (b -> c) -> (a -> b) -> a -> c` so that composition can be used at arbitrary choices of the types. So like, while we can use this composition function at any particular place we need composition, we can't define `compose` to have this type because the first use site will force the metavars to have a particular value and then we get a nasty global monomorphism. We need to explicitly have metavariables in the language itself, rather than at the metalevel of doing the synthesis/checking.
psygnisfive··on So you want to write a type checker (2014)
Ahh, well! That's a trickier problem! You need a bidirectional system that has unification for metavariables, and then some system for handling unsolved metavars. But to do that requires a more complicated set up. The goal of the post was to introduce the core ideas and show that it's relatively simple to do decent chunks of this stuff. :)
psygnisfive··on So you want to write a type checker (2014)
It was also front page on HN at the beginning of 2015 ;)
psygnisfive··on Proof Refinement Basics
Yeah, we're cross posting from my blog to the official IOHK blog, too. The first post only just got up on IOHK :p
psygnisfive··on Symbolic Machine Learning
Oh! Was Murray Shanahan's lab involved with this? Cool. I've chatted with Murray a very tiny bit on twitter about this all. That paper is part of what inspired me to write this blog post, because I was dissatisfied with the approach they propose.

It felt to me like they had found a way to restrict "symbolic" data to a very narrow domain where issues like hierarchical structure was totally absent, and vectorial representation was therefore quite straight forward, and I wanted to figure out an alternative. Instead of restricting the kinds of symbolic data involved, do the full spectrum. I had the symbolic vector idea in my head for about two years as an answer to the representation problem, but I hadn't seen what the right answer was to the other aspects, at least not clearly. But that paper motivated me to start thinking about it again, and this time I saw the answer. :)

psygnisfive··on Symbolic Machine Learning
That's correct, yes. Cycles don't affect subgraph counts. There's still only finitely many.
psygnisfive··on Symbolic Machine Learning
Reading a graph back can't be done with any certainty, nor is it intended to be done. It's a representation that's intended to be used to build inputs to ML systems, not outputs. Building symbolic outputs should be done via the other techniques mentioned in the blog post (eg. structural editing), that way you can take advantage of notions of correctness inherent in the symbolic representation.

Regarding handling lossiness, it's not clear to what extent it needs to be handled, but the `k` mentioned in the definition of symbolic vectors is a parameter, and the larger `k` is, the less lossy the representation.

psygnisfive··on Symbolic Machine Learning
Oh! Thanks for pointing this out. The whole site is hand maintained, and I routinely forget to put stuff up there. :)
psygnisfive··on Symbolic Machine Learning
I think to some extent it disappeared, to some extent it rebranded. But mostly it disappeared, because commercial motivations pushed a lot of money towards machine learning research. But that's just a hunch.
psygnisfive··on Symbolic Machine Learning
Grammar inference is a very interesting (tho quite different) topic. We have absolutely no idea how humans do it, and we know that its really really hard (nearly impossible!) to do given just raw text. Super interesting topic!
psygnisfive··on Symbolic Machine Learning
It's a very small unification, and a big, eye-catching claim.

Besides, I said "aims", not "succeeds"! :)

I certainly don't think this is The Big Solution, tho. It's far more mundane. Unifying the techniques is nice, but all that means is that we don't have to think about GOFAI and ML as fundamentally distinct. It doesn't mean that any truly deep problems have been solved, just that there's now a reasonably reliable way to use both that isn't just "simultaneous" but rather "fused".

psygnisfive··on Symbolic Machine Learning
I know of no other work like this, unfortunately.

But I would caution against saying this is a Vector Symbolic Architecture; the representations are, as far as I know, quite distinct.

psygnisfive··on Symbolic Machine Learning
Heyo. Author here.

It depends on what you mean by that. It assumes a fixed set of node labels, but not node identities, since we're counting subgraphs. So for instance, multiple distinct nodes labeled `X` or edges labeled `Y` will contribute to the same count, despite having distinct nodes involved.

psygnisfive··on Regex Edit Distance
The general idea here is that you can calculate not only whether or not a string matches a regex, but if it doesn't match, precisely by how much (in the minimal case).
psygnisfive··on Ask HN: Pick startups for YC to fund
Buy instant(ish) noodles from an asian grocery. They often have lots of great variety and are cheap and healthier than the ramen you'll usually get in big chain groceries. In fact, but as much as you can from asian groceries, they tend to be super cheap and need your business more than big chains do.
psygnisfive··on Grammars as Data Types
Gosh, people are really interested in this suddenly, huh? Well, I can answer any questions people may have! :)
psygnisfive··on Generic Evaluators – defining language-generic evaluators (lazy/eager/stack &c)
I'd caution the reader that this post is about purely functional, type theoretically defined languages. I haven't yet generalized to languages with implicit effects (tho I suspect it's possible). Explicit, type-defined effects via free monad-like setups are entirely possible with this, however.
psygnisfive··on Dynamic Languages Are Static Languages (2011)
As CHC says below, "dynamic" typing is no different. It's just a deferment of wrongth, not a lack of it.

But if I were to take a staunch SPJian-McBridian position, I would say this attitude arises from really useless type systems.

A good type system is EITHER capable of letting you say as little as necessary, and only telling you when something is messed up (like Haskell or ML, which have type inference and therefore don't require you to write types) OR is capable of letting you say what you mean, and then doing a lot of work for you.

This is the wonderful benefit of dependent types: you can say enough about your intention that you stop fighting the type checker, and actually get the type checker to do work for you.

This is really something that hasn't percolated into the mainstream of programming yet, but is slowing creeping into Haskell with typed holes, but in dependently typed languages like Agda or Epigram, types can be expressive enough that your editor can write half the program for you just because the type you wrote has only one program as its inhabitant.

McBride likes to describe it as, Dependent Types warp code space so that the direction we want to travel is "down", and all we have to do is let ourselves fall.

As an example, here's a demonstration of some simple (but exemplary) interaction with Agda. If we define this type:

    data Vec (A : Set) : Nat -> Set where
      Nil : Vec A 0
      Cons : forall {n} -> A -> Vec A n -> Vec A (1 + n)
where `Nat` is the type of natural numbers and `Vec` is the type of lists indexed by their length, then we might be inclined to write this function:

    append : forall {A m n} -> Vec A m -> Vec A n -> Vec A (m + n)
    append xs ys = {! !}0
where the `{! !}0` is a portion of the program that hasn't yet been defined, called a hole. We can put the cursor in the hole (hole 0) and ask the editor to do a case split on `xs` with `Control-c Control-c x`, and the program will change to be

    append : forall {A m n} -> Vec A m -> Vec A n -> Vec A (m + n)
    append Nil ys = {! !}0
    append (Cons x xs) ys = {! !}1
if we put the cursor in hole 0, we can hit `Control-c Control-a` (a for agsy, or auto) and itll fill in the hole with the solution `ys`, and if we do the same in hole 1, itll fill in `Cons x (append xs ys)`.

The type of the function we're defining is enough that agda can actually find the definition with almost no help from us.

Not knuckle wrapping here :)

psygnisfive··on JavaScript is the C++ of the Web
I wonder if this is a reanalysis of initial clipping. English lets you do some pretty aggressive deletion of initial segments of an utterance, and in many many cases that ends up being just a pronoun.. hmm
psygnisfive··on Dynamic Languages Are Static Languages (2011)
When Bob says that it's restrictive, what he means is simply that you cannot say more. Which is true -- you can't express things when your only type is "something". You're allowed to saying nothing, and that's it. And that's pretty darn restrictive!
psygnisfive··on Sierpinski Triangles in Bitwise Logic
I put together this little blog post showing how bitwise logic operators secretly have Sierpinski Triangles lurking in them. They also have other interesting patterns too, if you use different operators.
psygnisfive··on Error Correcting Parser with Edit Distances
Another post in my series on parsing malformed input. I think of all the ways of doing this, this approach works best, especially because you can pre-compute a lot of it.
psygnisfive··on A Jarvis-like AI for your apps, drones, robots [video]
I wrote a blog post sort of explaining it all http://www.languagengine.co/blog/you-must-be-nuts/
psygnisfive··on A Jarvis-like AI for your apps, drones, robots [video]
The bulk of it will be in the cloud. Aside from letting me make improvements that then get reflected in all apps LE is embedded in without updates to them, it also lets developers add new vocabulary and conversation patterns that they missed before, so that they can actually make their app's AI better without users having to update.

There are also interesting possibilities of cross-pollinating apps, so that as more developers use LE, its out-of-the-box capabilities grow. There's no reason, for instance, that developers should be re-inventing the wheel each time someone builds an app or a robot or whatever. Imagine if every human was born with the cumulative knowledge and skills of all previous humans. Now imagine you can do that with AI.

psygnisfive··on A Jarvis-like AI for your apps, drones, robots [video]
Speech processing is a secondary issue. Others are working on it, and it's basically a solved problem for the most part.

I don't know about SQL's natural language support, so I won't comment.

As for languages, the technology is independent of particular languages, so you can in principle add modules for, say, core Mandarin vocabulary, and then write your apps for Mandarin. I only speak English, however, so I can only add core vocab for that. :\

Page 1 of 4Next →