Infer.NET user guide : Fun

The Grammar and Semantics of Fun

Infer.NET Fun is a subset of well-typed programs in Microsoft Visual F#. A Fun program is a set of F# value definitions, and F# function definitions whose bodies are Fun expressions, as shown below.

In the following, let "f" range over F# function identifiers, "var" range over F# value identifiers, "field" range over the field names of F# records, "integer-literal" range over F# integer literals, "float-literal" range over F# floating-point literals, and "bool-literal" range over the F# booleans, true and false.

First, we give the grammar of Fun value types, the F# types of the bodies of Fun functions. Fun value types do not include function types, so functions cannot return functions as values. We do not make it explicit in the grammar below, but types may refer to F# type definitions by name. Recall also that F# record types need to be introduced by a type definition before use.

    type ::=                                // Fun value type
      unit                                     // unit
      bool                                     // boolean
      int                                      // integer
      double                                   // floating-point
      (type1 * ... * typeN)                    // tuple
      { field1: type1; ...; fieldN: typeN}     // record
      type[]                                   // array

Next, we give the grammar of Fun programs and function definitions.

    program ::= constant1 ... constantN function1 ... functionM            // Fun program
    constant ::= let c = fsharpExpr                                        // Fun constant
    function ::= [< ReflectedDefinition >] let f (var1, ..., varn) = expr  // Fun function definition

Each function must have the ReflectedDefinition attribute so that Fun inference routines can find the parsed syntax tree of the function's body at run time. Constants are computed at compile time, and only their values are included in the model. This allows constant definitions to be arbitrary F# expressions, without restrictions. A typical application would be a constant that gets its value from a file or a database.

Next, we list the grammars of expressions expr and distribution expressions dist below. An expression, such as f (expr1, ..., exprN), may refer to an F# function f in scope, provided that the definition of f has been marked [< ReflectedDefinition >], and that the body of f is a Fun expression.

    expr ::=                                // Fun expression
      var                                       // variable
      f (expr1, ..., exprN)                     // function call to F# function f
      integer-literal                           // integer literal eg 42
      float-literal                             // float literal eg -1.0
      bool-literal                              // bool literal, true or false
      { field1 = expr1; ...; fieldN = exprN }   // record expression (N>=0)
      ( expr1, ..., exprN )                     // tuple expression (N>=0)
      [| expr1; ...; exprN |]                   // array expression (N>=0)
      expr.field                                // record lookup
      fst(expr)                                 // first projection
      snd(expr)                                 // second projection
      expr1.[expr2]                             // array index
      not expr                                  // negation
      expr1 && expr2                            // conjunction
      expr1 || expr2                            // disjunction
      expr1 = expr2                             // equality
      expr1 <> expr2                            // disequality
      expr1 < expr2                             // less than
      expr1 <= expr2                            // less than or equal
      expr1 > expr2                             // greater than
      expr1 >= expr2                            // greater than or equal
      -expr                                     // unary minus
      expr1 + expr2                             // addition
      expr1 - expr2                             // subtraction
      expr1 * expr2                             // multiplication
      expr1 / expr2                             // division
      for var in expr1 do expr2                 // iteration loop
      [| 0 .. expr |]                           // integer range array expression
      range(expr)                               // indexes of an array; equals [| 0 .. expr.Length - 1 |]
      [| for var in expr1 -> expr2 |]           // array comprehension expr1 expr2                     // zip two arrays
      let var = expr1 in expr2                  // let expression
      if expr1 then expr2 else expr3            // conditional expression
      expr1; expr2                              // sequential expression
      random(dist)                              // draw from distribution
      observe expr                              // observation
      expr : type                               // type annotation

    dist ::=                                // Fun distribution

There are some restrictions on the kind of expressions used as array indexes. A valid index expression is either a loop iterator or an integer array indexed by a valid index expression. There are also restrictions on the use of equality for floats: it is only allowed in expressions of the form observe (f1 = f2).

The semantics of Fun programs and expressions is the same as in F#, with two additions. First, an expression random(dist) draws a sample from the Fun distribution dist, defined in terms of Infer.NET distributions. Second, an expression observe expr is a constraint that the bool expression expr must evaluate to true. In general, the semantics of an expression of type T is a distribution over values of type T, conditioned on any contained observe expressions being valid.

A Fun program can be executed directly to compute random samples, or passed to Infer.NET to compute probability distributions.

  • Suppose we have a Fun function f of type T -> (T1 * ... * TN), that is, a function from an argument T to a tuple with components T1, ..., TN. The body of f is an expression defining a joint probability distribution over the types T1, ..., TN, conditional on the argument of type T. Suppose V is an F# value of type T. If we simply run f V we get samples from this distribution, conditioned on V, but with all observations ignored. Running sample f V takes observations into account. It returns Some a with a sample a if all observations succeed and None if an observation fails.
  • Alternatively, to get a representation of the conditional distribution f V, we run let (d1,...,dN) : (IDistribution< T1 > * ... IDistribution< TN >) = infer <@ f @> V, which invokes Infer.NET to compute the marginal distribution of type IDistribution< Ti > for each component of the distribution, conditioned on V. Note that the type annotation indicating the marginal distributions is required; this type is used to guide infer's operation.

(The F# syntax <@ f @> is a typed quotation, of type Quotation.Expr< T -> (T1 * ... * TN)>. The function sample is in module MicrosoftResearch.Infer.Fun.FSharp.Syntax. The function infer (and related functions inferFunN (for N:1..4) and inferDynamic) are in module MicrosoftResearch.Infer.Fun.FSharp.Inference. The interface IDistribution is in namespace MicrosoftResearch.Infer.Distributions.)

The example above assumes the distribution induced by f is over a tuple type T1 * ... * TN where the marginal distributions are represented by a tuple IDistribution<T1>*...*IDistribution<TN>.

In general, we have a type CompoundDistribution (in module MicrosoftResearch.Infer.Fun.Core.Inference) to represent collections of marginals of joint distributions over Fun value types. A compound distribution, a value of CompoundDistribution, is either an IDistribution, a record or tuple of compound distributions, an array of compound distributions, or unit. Hence, we have a second mechanism for inference on functions.

  • Consider a Fun value type T2, a Fun function f with type T1 -> T2, and an F# value V of Fun value type T1. To obtain a representation of the conditional distribution f V, we run let cd = inferDynamic <@ f @> V, which binds a collection of marginals of type T2 to cd of type CompoundDistribution.

To get started with inference, Samples\Fun\QuickStart.fsx has an example of calling inferFun2 on a function coins returning pairs, and Samples\Fun\Reference.fsx has an example of calling inferDynamic on a function coins returning a record, with a helper function to decompose the resulting CompoundDistribution into its components.

©2009-2013 Microsoft Corporation. All rights reserved.  Terms of Use | Trademarks | Privacy Statement