psygnisfive

Since most (all?) devices now have speech recognition built in, this'll plug into those easily. I'm also going to let developers plug their own in if they have better stuff than Google etc

I'm working to make it so that there's basically no real API for the vocabulary at all, you just use a little widget on the site to specify exactly the relevant functionality your app supports, and how the word realizes that, with nice visual linkages. LE will then pull that info into the logical formalism. No API needed, just some clicks.

Ideally, it should be so simple that I can make a 2 minute video of it and by the end, you'll think "well that was obvious", as opposed to "ugh now I have to learn type theory? ffs"

I did a dopey little sketch on of the idea, fwiw https://twitter.com/psygnisfive/status/558287230662615040

What? I don't know what you're talking about. ::whistles innocently::

Getting it to a state, even the minimal one, where it's ready for launch has taken slightly longer than expected. :(

Right now I'm reworking the API a little bit. I realized that the means of specifying new vocabulary for it was not at all friendly for coders who don't have lots of type theory background. I have a new way of doing this that I think will work, and it'll be up hopefully within a few weeks.

yeah, people have suggested a variety of things. i'll add those to my list of static generators to investigate, thanks :)

I'm working on it, have no fear! I'm hand coding the blog right now because I don't want to use a CMS, I really don't like the options I have. I might just hand-code an RSS feed.

Actually this isn't true, wrt Chomsky. Chomskyan linguistics assumes statistics is very important (and this has been noted by Chomsky himself since at least the early 1960s). Chomsky simply argues that statistics is insufficient on its own. And in truth, most NLPers believe this, but they rarely admit it. Most/all NLP projects have some form of "universal grammar", tho usually its something like a regular grammar (~ a Markov chain) or at best a probabilistic CFG (PCFG). I suspect the reason is that, to some extent, hierarchical structures like this seem so natural that its hard to imagine what else you could do, so there's a tendency to co treat CFGs as not even a grammar choice, but it is. There are other kinds of grammars (such as pregroup grammars) which lack these notions of hierarchy but work perfectly well for the same domains as CFGs, just in very different ways.

It depends on the kind of dependency trees. I've seen plenty of semantic-y dependency trees and plenty of syntactic-y dependency trees. I'm not sure how common either really are ever, but on the semantics side, it's the best you get, usually, and isn't all that good for semantics. It's fine for syntax, more or less.

I think they're saying tho that in one case "bread" means a kind of food, and in the other, it means money. If the different uses were more directly connected to particular words that could disambiguate, it wouldn't be too hard -- head features typically can do this -- but the disambiguation here is far more conceptual in original. You know that you need money to buy things, and so you know that not having money is a good reason for not being able to buy things. But bread-the-food is not needed to buy things, so not having it isn't a good reason for not being able to buy things. So probably the second "bread" is the bread-money version. This kind of disambiguation is super tricky without broader world knowledge.

Well let me know what sorts of things you have in mind, and what you can't find in other services! I'll see if there's something LE can do for you, or could do in the near future. I'm always in the irc channel (#languagengine on freenode), so feel free to drop by. :)

Yep, I agree with what you say. Tho I would dispute calling a POS gloss much of a structure. When I think structure, I think full syntax. Parse + formal features. Or a full logical formula for the semantics! Now that's structure!

Well, if you'd like to know what I think we'll be doing in the future, check out the rest of the site. :p

But: I'm building an SDK for conversational AI (think Siri, in any app, and 10 times better), that's what the site as a whole is for. I think in 5 years it'll be pretty commonplace to have fairly natural, Jarvis-like conversations with computers, and within 10 years we'll have R2D2/C3PO robots.

It really depends on what you count as syntactic and semantic information. As a linguist, to me syntactic information is tree structures, syntactic categories, etc., and semantics is formulas in some (typically higher-order) logic. But for a lot of the NLP that I see, "syntax" is pretty shallow stuff like head words and POS tag contexts, and "semantics" is at best things like word vectors maybe dependency trees. These are very different. But maybe we're thinking of different things! :)

I think it's going to be machine learning too, just over richer structures. And actually when you need parsing that's what you get together. But few people need real parsing right now. Some things, like meaning, will I think have to be more old school. There's no good way to learn meanings right now at all.

I try. :) I've written some related stuff on the blog there, if you want more (most of it I've linked here on HN?)

I'm gonna try to write more often, so hopefully I'll keep giving you interesting reads! :)

Yep, it's certainly true that these techniques never went away fully, but they've been eclipsed by the simpler techniques. Academic work, especially under the guise of "computational linguistics" as opposed to "NLP", works a lot on this. But the public face of NLP has been pure new-school stuff for a while now.

I was more trying to just talk about why the richly structured old school fell from grace, not claim that it's dead and buried.

to find out which 42, we'll need to build a computer the size of a planet

awesome! what sorts of things does NetBase do with old school NLP?

A follow-up to my "So you want to learn type theory" reading list. Here I show you how to write a simple type checker using JS.

Aside from PFPL, which is oriented towards implementors of programming languages, type theory has practical uses in the act of programming itself. That is to say, with an adequate type theory, you can at a minimum use it to help you construct proofs that your programs do what you want them to do. But that's doable with any meta-system for certified programming, TT is just one particular meta-system that has some nice properties.

The more common practical uses are:

1) If you're using a statically typed language, knowing some basic TT will let you understand the hows and whys of its type system. This is especially true of static langs that have richer type systems, like Haskell.

2) Rich type systems actually help you program! a lot of people complain that type systems merely complain when you mess up -- which is helpful, because you now know you've messed, but not completely helpful because it feels like the types don't help you. The truth is,, this is mostly true only of BAD type systems.

A GOOD type system can guide you to the right answer by making the number of possible programs very tiny. Instead of infinitely many programs, there might just be one or two.

A GOOD type system can guide you to the right answer by making it possible for the computer to write parts of the program for you because the types make it obvious what the options are at any moment program construction.

For specific examples, you'd have to look around. I don't have any offhand (nor am I trying to convince you to learn TT!). Conal Elliot and Edward Kmett no doubt have plenty of good examples, or could tell you who does.

Ahh this is a very good question.. I'll give two answers, the first more philosophical and the second more example-driven, and both hesitant, 'cause I'm not sure anyone's really thought about deeper why's like this much. :)

1:

My first answer is, because of the nature of what a logic is. Logics are systems for reasoning about some problem domain, or put it another way, logics are ways of convincing yourself that you're justified in believing a judgment (`A is true`, `B is a proposition`, `C is tasty`).

What this means is that, to have a proof `M` which proves a judgment `J`, is to have some piece of data which you can look at. So all proofs are some kind of data, in the same way that all novels and all movies are some kind of data.

A harder question is why all data is a kind of proof and that's more subtle. Some people actually want to say they're not, proofs are just a special kind of data, while others want to just say to loosen the notion of proof and proposition. I don't think there's a good answer for this direction.

2:

My second answer is, it turns out they couldn't be anything else! Consider the inference rule (written in natural English):

    if you know
      A is true
    and you know
      B is true
    then you can conclude
      A&B is true

which tells you when you can make the judgment `A&B is true`. When you use this rule, you have to supply two justifications of the premises `A is true` and `B is true`. That is, you have to provide two pieces of evidence, two proofs, one for each premise.

Now consider this description of how to make pairs:

    if you have
      M of type A
    and you have
      N of type B
    then you can make
      (M,N) of type A*B

Here we're just describing how pairs are formed: you take two things, and stick them together with a constructor to form a new piece of data.

Now I ask you, what are you doing when "proving A&B" if not taking two things (two smaller proofs of `A` and `B`) and sticking them together to form a new piece of data (the proof of `A&B`)? I would argue you're not doing ANYTHING different. The act of proving a conjunction is just the same as the act of making a pair!

Now do this for other logical connectives:

    proving a disjunction is just the same as giving an element of a tagged union

    proving an implication is just the same as giving a function

    proving the trivial proposition is just giving a 0-length tuple

    proving the absurd proposition (which is impossible)
      is just giving a void-type value (which is impossible)

So why are type theories a logic? Well just look!

----

Now, I should say, this connection does not mean that all logics are type theories! Type theory has a very specific view of how inference rules are justified, by appeal to certain principles which turn out to be computational in nature.

Why these principles should be so powerful as computational principles, I don't know. It's a mystery. Maybe God is a type theorist? ;p

One of the primary major players with generics in Java is Philip Wadler, a type theorist and one of the co-creators of Haskell. Generics comes straight out of type theory research, and normally its called parametric polymorphism, but mainstream programmers can't handle that funky terminology. Apple's work on Swift has openly acknowledge its debt to Haskell and contemporary work on type theory, and it shows. As for the rest, you'd have to ask the people who worked on them.

At any rate, C++, Scala, Rust, Java.. these are not languages that take type theory very seriously, and probably couldn't. It's certainly true that the popular imperative languages don't take TT seriously.

But so what? The comment was about general purpose languages, and type theory is demonstrably of use in implementing them. Just because most mainstream languages don't use type theory doesn't make that not true. It just means most mainstream languages do not make use of everything they could.

Oh well. Their loss.

Oh wow, I saw the United Therapeutics HQ in Silver Spring being built, walked around it a bunch when it was done, thought it was a cool building, etc. and had no idea it was Rothblatt's company. Neat!

Speaking of The Bubble, there's a documentary on YouTube filmed shortly after/during the burst. https://www.youtube.com/watch?v=EsVpNB2Lv3U

At one point you see these things, pink slip parties.. fascinating stuff. http://www.investopedia.com/terms/p/pink-slip-party.asp

Anyway, we're not in a bubble, so don't worry. :)

Thats also an appropriate analogy, I think. The main point is, type theory is a tool for reasoning, while set theory is a thing reasoned about. At least in the context of foundational questions. You can flip them, but then it becomes kind of silly, imo.

Yep, that's a perfect analogy. And people have actually used type systems to formalize the concept of units. :)

This is really not true at all. Unless what you mean by "implementing type systems for general purpose languages" is a sort of weak, generally useless type system that punishes rather than helps.

This is ESPECIALLY false of Pfenning and co's work, which is aimed specifically at understanding how to apply type theoretic techniques to the design of PLs, so that you get a PL with exactly the sort of stuff you want.

I added a link to the page to PFPL, which is an entire book on how to implement programming languages using type theoretic tools. It even has sections on OO programming, if you're into that sort of thing. It's all the same toolkit, in the end.

So I think you're right that you should have a good reason. Fashion isn't enough. Don't learn TT cause its "cool", that would be stupid.

For FP, tho.. I would say that you'll be a better functional programmer by knowing TT, even if you don't have a typed language. And if you do have a typed language, you'll want to understand your type system, so learning TT gives you the tools to do that properly.

But there's more than just that. Types offer a lot to the programmer from a practical perspective. Forget the whole thing about using types to prove your code works. You can do that, you can do certified programming if you want. Learn Coq, it's great for that. But types offer you something else:

    *** types help you figure out what the right program is ***

This is something that is often ignored or overlooked, but it's very important. Conor McBride (who's work you might want to look into once you know some TT) talks about this a lot.

A relatively trivial, but easy-to-understand example of this would be the simple programming problem of writing a program that can take a pair of type `A * B` (where `` is the pair product) and return a pair of type `B A`. That is, the flips its argument's elements around. Ok this is simple and we all know what the program is, right, but let's do a little programming in Agda to see how types help you here.

We'll start with a type declaration for the function, and the LHS of an equation that defines the function:

    swap :: A * B -> B * A
    swap p = {! !}0

Notice I put in this funny thing `{! !}0`. This is called a "hole": it's a part of the program that's missing. The 0 indicates its identity (this is hole 0). If we put the cursor in the hole, we can ask Agda to tell us about the hole, and it'll reply:

    Goal: B * A
    Context:
      p : A * B

The goal is the type of the value we have to supply for the hole, the context is all the variables in scope, together with their types.

Now, still with the cursor in the hole, we can ask Agda to pattern match on `p` and split the equation into as many patterns as it can. Because we have types, Agda knows all of the constructors that a type has, so it can automatically fill in the patterns for us. Since pairs have only one constructor, we simply get a slightly more complicated equation:

    swap :: A * B -> B * A
    swap (x , y) = {! !}0

Now let's again ask Agda about the hole:

    Goal: B * A
    Context:
      x : A
      y : B

Notice: `p` is gone, because we matched on it, and instead we have `x` and `y`, new variables binding the elements of the pair, and their types.

Now let's ask Agda to try filling in the hole a little bit. We can tell Agda to refine the hole, and because it knows the goal is a pair type, and pairs have exactly one constructor, it can chose that constructor to fill in part of the program for us:

    swap :: A * B -> B * A
    swap (x , y) = ({! !}1 , {! !}2)

Now we have two new holes, with goal types B and A respectively, and the same contexts as before. We can again ask Agda to work on these holes, and it will fill in:

    swap :: A * B -> B * A
    swap (x , y) = (y , x)

And we're done, we have a definition. And notice: the only code we wrote was to specify the type of `swap`, and put in an initial equation. The rest of the program came from Agda looking at the types, and then doing stuff based on that. This is a simple example, but it's exemplary of the "conversational" back and forth between the programmer and the type checker that you can get in a strongly typed program, where the types can actually help you FIND the right program.

Just as another more obnoxious example, here's the the type for an induction principle for lists (also called dependently typed "fold", or dependently typed "reduce", or whatever):

    listInduction : (A : Set) (P : List A -> Set)
                 -> P []
                 -> (forall (x : A) (xs : List A) -> P xs -> P (x :: xs))
                 -> forall (xs : List A) -> P xs
    
    listInduction A P n c xs = {! !}0

You can do the same thing as before, button mashing until you have no more holes, with this, and you get the right answer. In fact, there are exactly two right answers, and you can get both depending on a choice of which mashing you do. At no point do you actually have to figure out yourself that the following program is a solution:

    listInduction A P n c []        = n
    listInduction A P n c (x :: xs) = c x xs (listInduction A P n c xs)

because the type FORCES that to be one of only two solutions. This kind of ability to button-mash and get a correct solution has actually lead people to compare dependently typed programming to playing a video game.

The moral is: with strong types, the types HELP you, rather than smack you on the knuckles when you've messed up. So there really is something beyond just fashion and whim. It's actually practical!

I'll start added recommendations to the link, so keep 'em coming.

I want to disagree a little bit with chas here and just say that type theory as we know it today emerged out of a different, post-computer tradition than old-school Russellian type theory. Modern type theory comes arguably from Martin-Löf and the FP domain.

As for what is type theory vs. set theory vs. category theory, I'd put it this way: type theory is a flavor of proof theory built on computational justification of inference rules and patterns of reasoning. But that's maybe a bit boring sounding, so another way to think of it is, type theory is a framework for thinking about what makes sense in a strongly typed programming language. Most PLs with types just throw types in as an afterthought, whereas a type theoretic perspective says, start with the types, use the types to express what you want the programming language to do, and the lambda calculus that you get from this is your programming language.

What sets it apart from set theory is that type theory is much more about inference and justification. Set theory is more a theory about sets, where you presuppose these things exist and have properties (membership, etc.) that you want to capture and reason about. Type theory, on the other hand, is a way of thinking about how to invent new sorts of things, and a tool for reasoning in and of itself. You reason about sets using some logic, type theory is a logic.

Something similar is true about category theory as well, only for a different sort of thing (whereas sets are defined by membership, etc. categories are defined by objects and maps, etc.)

A good analogy, I would argue, is this:

    type theory : set theory/CT  ::  mathematics : physics

One is a general framework of reasoning, inference, proof, etc. the other is a domain that you apply it to. It's not a perfect analogy for all the obvious reasons, but thats roughly how I'd suggest you think about it. When you do your set theory, you take for granted all the stuff like conjunction, implication, quantification, etc. just as the language you use to talk about sets. With type theory, you're looking at those very linguistic constructs.

This one is I guess less about implementing LE than it is about how to implement things in LE, but whatever. Maybe next time I'll say "devblogging" to be more generic. heh