Math Limericks

I thought I’d try my hand at a small collection for Hindley–Milner.

    [Var]
    When given a var’iable X
    that’s already in the context
    with some type called T
    then obviously
    that T is the type of that X.

    [App]
    Encountering two terms abreast
    where the former’s a function, you test
    that the function can take
    what the argument makes;
    its result gives the type of the rest.

    [Abs]
    The term “lambda from X to E”
    infers as the type A to B
    if the context, extended
    with X represented
    as A, says E typechecks as B.

    [Let]
    The type that is lastly inferred
    when a term’s bound with “let” to a word
    —and the body can cope
    with that name bound in scope—
    is the type that the body incurred.

    [Inst]
    If you don’t find it too esoteric
    and you happen to have some barbaric
    too-general expression
    then at your discretion
    you can choose a type that’s less generic.

    [Gen]
    If the type of a term could abide
    any type that a user supplied,
    and the name occurs not
    free in context, you’ve got
    a type var that’s forall-quantified.

The meter could stand some improvement, but nobody expects limericks to be perfect.

A favorite of mine:

  There once was a young lady named bright
  Whose speed was much faster than light
  She set out one day
  In a relative way
  And returned on the previous night.