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!

0Thread HN

So you want to write a type checker (2014) 9 years ago

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)

0Thread HN

So you want to write a type checker (2014) 9 years ago

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.

0Thread HN

So you want to write a type checker (2014) 9 years ago

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. :)

0Thread HN

So you want to write a type checker (2014) 9 years ago

It was also front page on HN at the beginning of 2015 ;)

0Thread HN

Proof Refinement Basics 9 years ago

Yeah, we're cross posting from my blog to the official IOHK blog, too. The first post only just got up on IOHK :p

0Thread HN

Symbolic Machine Learning 10 years ago

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. :)

0Thread HN

Symbolic Machine Learning 10 years ago

That's correct, yes. Cycles don't affect subgraph counts. There's still only finitely many.

0Thread HN

Symbolic Machine Learning 10 years ago

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.

0Thread HN

Symbolic Machine Learning 10 years ago

Oh! Thanks for pointing this out. The whole site is hand maintained, and I routinely forget to put stuff up there. :)

0Thread HN

Symbolic Machine Learning 10 years ago

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.

0Thread HN

Symbolic Machine Learning 10 years ago

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!

0Thread HN

Symbolic Machine Learning 10 years ago

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".

0Thread HN

Symbolic Machine Learning 10 years ago

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.

0Thread HN

Symbolic Machine Learning 10 years ago

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.

0Thread HN

Regex Edit Distance 10 years ago

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).

0Thread HN

Ask HN: Pick startups for YC to fund 10 years ago

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.

0Thread HN

Grammars as Data Types 10 years ago

Gosh, people are really interested in this suddenly, huh? Well, I can answer any questions people may have! :)

0Thread HN

Generic Evaluators – defining language-generic evaluators (lazy/eager/stack &c) 11 years ago

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.

0Thread HN

Dynamic Languages Are Static Languages (2011) 11 years ago

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 :)

0Thread HN

JavaScript is the C++ of the Web 11 years ago

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

0Thread HN

Dynamic Languages Are Static Languages (2011) 11 years ago

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!

0Thread HN

Sierpinski Triangles in Bitwise Logic 11 years ago

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.

0Thread HN

Error Correcting Parser with Edit Distances 11 years ago

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.

0Thread HN

A Jarvis-like AI for your apps, drones, robots [video] 11 years ago

I wrote a blog post sort of explaining it all http://www.languagengine.co/blog/you-must-be-nuts/

0Thread HN

A Jarvis-like AI for your apps, drones, robots [video] 12 years ago

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.

0Thread HN

A Jarvis-like AI for your apps, drones, robots [video] 12 years ago

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. :\

0Thread HN