Infers.Toys Library Reference

[<AutoOpen>]
module Basic =

type Eq<'x, 'y>

Equality: Eq<'x, 'y> is derivable when 'x unifies with 'y.

type Eq<'x, 'y, 'z>

Ternary equality: Eq<'x, 'y, 'z> is equivalent to And<Eq<'x, 'y>, Eq<'y, 'z>>.

type Basic =

Basic rules for logic programming: equality (Eq<...>) and disjunction (Choice<...>).

[<AutoOpen>]
module Bitwise =

type Bitwise<'b, 't> = {

Isomorphism between 't and 'b, which is either byte, int16, int32 or int64.

It would be more logical to map bitwise types to unsigned integral types. However, except for byte, unsigned integral types are rarely used in user defined types. A generic based on handling the signed integral types and bytes directly and the unsigned integral types bitwise is likely to be faster and more practical.

type Bitwise =

static member Float32: Bitwise<int32, float32>

This is very slow. Pull requests are welcome!

[<AutoOpen>]
module Elems =

Provides generic functions similar to, but not exactly like, Neil Mitchell's Uniplate.

The operations in the Elems module work most conveniently on recursive union (sum of products) types of the form

type SoP<...> =
 | Case1 of Elem<I1, J1> * ... * Elem<I1, Jm1>
 | ...
 | CaseN of Elem<In, J1> * ... * Elem<Im, Jmn>

where the Elem<_, _> types are not compound types such as list<SoP<...>> or SoP<...> * SoP<...>. This is because the primitive elems and subst operations do not look inside the Elem<_,_> types. Aside from recursive union types, many Elems operations work on (non-recursive) unions, (recursive or non-recursive) records and (never recursive) tuples.

In the documentation we will make use of the following type:

type BinTr<'x> =
  | Lf
  | Br of BinTr<'x> * 'x * BinTr<'x>

Note that Elems is not limited to manipulating binary trees. Binary tree is merely used as an example of a simple recursive datatype.

val elems<'h, 'w> : 'w -> array<'h>

elems<'h, 'w> w returns an array of the immediate elements of type 'h in w.

By design, elems does not look inside the elements of 'w. The following examples should help to clarify what this means:

elems<int, _> Lf = [||]
elems<int, _> (Br (Lf, 1, Lf)) = [|1|]
elems<int, _> (Br (Lf, (1, 2), Lf)) = [||]
elems<int * int, _> (Br (Lf, (1, 2), Lf)) = [|(1, 2)|]

Note that any type of elements 'h can be queried, including the input type 'w. For example, elems<BinTr<int>, _> (Br (Lf, 1, Lf)) gives [|Lf; Lf|].

val children: 'w -> array<'w>

children is equivalent to elems<'w, 'w>. children only makes sense when applied to a recursive union or record type. For example, children (Br (Lf, 1, Br (Lf, 2, Lf))) gives [|Lf; Br (Lf, 2, Lf)|].

val elemsDn<'h, 'w> : 'w -> seq<'h>

elemsDn<'h, 'w> w returns a sequence of all the elems of type 'h in w and recursively in the children of w.

For example,

elemsDn<int, _> (Br (Br (Lf, 1, Br (Lf, 2, Lf)), 3, Br (Lf, 4, Lf)))

gives the sequence

seq [3; 1; 2; 4]

val universe: 'w -> seq<'w>

universe w is equivalent to Seq.append (Seq.singleton w) (elemsDn w).

For example,

universe (Br (Br (Lf, 1, Br (Lf, 2, Lf)), 3, Br (Lf, 4, Lf)))

gives the sequence

seq [Br (Br (Lf, 1, Br (Lf, 2, Lf)), 3, Br (Lf, 4, Lf))
     Br (Lf, 1, Br (Lf, 2, Lf))
     Br (Lf, 4, Lf)
     Lf
     Br (Lf, 2, Lf)
     Lf
     Lf
     Lf
     Lf]

val para: ('w -> array<'r> -> 'r) -> 'w -> 'r

para w2rs2r w performs a fold-like computation called a paramorphism.

For example,

let height t = para (fun _ hs -> Array.fold max 0 hs + 1) t

computes the "height" of any recursive union or record type. For example, height gives

height Lf = 1
height [] = 1
height ("Non", ("recursive", "type")) = 1
height (Br (Lf, 1, Br (Lf, 2, Lf))) = 3
height [1;1;1] = 4

val subst<'h, 'w> : ('h -> 'h) -> 'w -> 'w

subst h2h w returns a new value of type 'w which is like w except that every immediate element h_i of type 'h in w is replaced with h2h h_i. elems >> Array.map h2h is equivalent to subst h2h >> elems.

val descend: ('w -> 'w) -> 'w -> 'w

descend is equivalent to subst<'w, 'w>. descend only makes sense when applied to a recursive union or record type.

val substUp<'h, 'w> : ('h -> 'h) -> 'w -> 'w

substUp<'h, 'w> h2h w performs a bottom-up transformation of the given value w, recursively descending into w and then substituting with h2h.

For example,

substUp ((+) 1) [1; 2; 3] = [2; 3; 4]

and

substUp (fun xs -> 0::xs) [1; 2; 3] = [1; 0; 2; 0; 3; 0]

val transform: ('w -> 'w) -> 'w -> 'w

transform w2w w is equivalent to w |> substUp w2w |> w2w.

For example, given type of a binary trees

type BinTr<'x> =
  | Lf
  | Br of BinTr<'x> * 'x * BinTr<'x>

we can write a function to mirror trees

let mirror bt =
  transform <| function Lf -> Lf
                      | Br (l, x, r) -> Br (r, x, l)
            <| bt

Now

Br (Br (Lf, 1, Lf), 2, Br (Br (Lf, 3, Lf), 4, Lf)) |> mirror

evaluates to

Br (Br (Lf, 4, Br (Lf, 3, Lf)), 2, Br (Lf, 1, Lf))

val rewrite: ('w -> option<'w>) -> 'w -> 'w

Transforms with given partial function until a fixed point is reached.

[<AutoOpen>]
module GFlip =

val gflip: ('a -> 'b) -> ('c -> 'd)

Derives a function that reorders, i.e. "generically" flips, the arguments of a given function. For example, gflip (sprintf "%s %d %c!") 2 'U' "Hello" = "Hello 2 U!".

Note that if the arguments do not have unique types the resulting ordering may not be the one you want.

Due to limitations of the F# type system, the function must have a monomorphic type. If the function does not have a monomorphic type, you must constrain it.

[<AutoOpen>]
module GUncurry =

val guncurry: ('a -> 'b) -> ('c -> 'd)

Derives a function that uncurries a given n-ary curried function. For example, guncurry (sprintf "%d %s") (1, "a") = "1 a".

Due to limitations of the F# type system, the function must have a monomorphic type. If the function does not have a monomorphic type, you must constrain it.

[<AutoOpen>]
module Integral =

type Integral<'t> =

Provides information on the integral type 't.

[<AutoOpen>]
module Json =

Provides a mapping between a subset of F# and JSON values. The goal is to make it possible to map typical existing JSON APIs to F# types and to specify new JSON APIs using F# types.

Note that the goal here isn't to provide an encoding of all F# types in JSON. Such encodings can be useful for the internal communication or persistence of an application, but tend not to work well for mapping existing JSON APIs or for specifying new APIs to be used by external applications. Neither is the goal to support entirely arbitrary JSON mapping, although one can always fall back to the JSON AST, but to rather provide a mapping that should lead to usable F# types when mapping typical APIs.

A mapping is always specified as a F# type. In the following we specify the (almost) bidirectional translation of the supported subset of F# values to JSON values.

Simple values are translated as is:

                     [< true >]  ~  true
                    [< false >]  ~  false
               [< number:int >]  ~  number
             [< number:float >]  ~  number
             [< number:int64 >]  ~  number
                 [< "string" >]  ~  "string"

Special numbers are translated to null and the translation is obviously not bidirectional:

                 [< nan:float>]  ~  null
            [< infinity:float>]  ~  null
           [< -infinity:float>]  ~  null

Note that special numbers do not have standard representation in JSON and the above treatment of special numbers corresponds to what JavaScript's JSON.stringify does by default. If you need to translate special numbers more intelligently, you need to do it explicitly.

The unit value, (), is translated to null:

                       [< () >]  ~  null

Records are translated to objects where record fields of option<_> type are considered optional properties:

  [< {l1 = v1; ...; lN = vN} >]  ~  {[< "l1": v1 >], ..., [< "lN": vN >]}

              [< "l": None   >]  ~
              [< "l": Some v >]  ~  "l": [< v >]
              [< "l":      v >]  ~  "l": [< v >]

Note that option<_> types are only treated specially when they are fields of record types (or labeled elements of a union case as specified below). One might expect to able to use option<_> types anywhere and to have None translated to null, but that would lead to a kind of ambiguity when trying to map an object property that has null as a valid value.

Tuples are translated to fixed length arrays with non-uniform types while lists and arrays are translated to arrays with uniform type:

          [<  (v1, ..., vN)  >]  ~  [[< v1 >], ..., [< vN >]]
          [<  [v1, ..., vN]  >]  ~  [[< v1 >], ..., [< vN >]]
          [< [|v1, ..., vN|] >]  ~  [[< v1 >], ..., [< vN >]]

Union cases are translated by ignoring the union constructor C and treating the carried value(s) either as a value by itself or as a record:

                      [< C v >]  ~  [< v >]
[< C (l1 = v1, ..., lN = vN) >]  ~  {[< "l1": v1 >], ..., [< "lN": vN >]}

That union constructors are ignored makes it possible to use them in encodings of both discriminated and non-discriminated unions. For the purpose of encoding typical discriminated unions, the special Is<_> value is translated to a string constant:

             [< Is<TypeName> >]  ~  "TypeName"

Maps and dictionaries whose keys are strings are translated to objects:

      [< map [("k", v); ...] >]  ~  {"k": [< v >], ...}
     [< dict [("k", v); ...] >]  ~  {"k": [< v >], ...}

Finally, JSON AST values are traslated to JSON:

                  [< Obj map >]  ~  [< map >]
                [< List list >]  ~  [< list >]
          [< String "string" >]  ~  "string"
          [< Number "number" >]  ~  number
                [< Bool bool >]  ~  [< bool >]
                      [< Nil >]  ~  null

type Obj = Map<string, Value>

Represents a Json object.

and Value =
  |    Obj of Obj
  |   List of list<Value>
  | String of string
  | Number of string
  |   Bool of bool
  |    Nil

Represents a Json value.

[<AutoOpen>]
module MayBeMutable =

val mayBeMutable<'t> : bool

Determines whether a value of the given type may contain mutable objects.

[<AutoOpen>]
module PU =

This is a toy example of a binary pickler / unpickler. This can handle integral types, floats, strings, tuples, records, and union types. Recursive types, such as lists, and recursive values, via records, are supported. Other types, including arbitrary classes or structs, are not supported.

This could be improved in various ways. Examples:

- Pickles do not contain any error checking information. It would be straighforward to add, for example, a hash of the type structure to the beginning of the pickle and verify it when unpickling to help to detect type errors.

- Support for various special types such as arrays and refs is not implemented. Such support could be added in a straightforward manner.

- Lists are pickled via naive recursive encoding. Lists could be implemented via (not yet implemented) array support.

Perhaps the main point here is that it doesn't really take all that much code to implement a fairly powerful pickler.

val pickle<'x> : 'x -> array<byte>

Converts the given value to an array of bytes.

val unpickle<'x> : array<byte> -> 'x

Converts an array of bytes produced by pickle into a value. The type of the result must match the type that was given to pickle.

module Product =

Generic functions for ad hoc record manipulation.

val get: 'p -> 'e

Gets an element of type 'e from the product of type 'p. If the product has multiple elements of type 'e it is not specified which element is returned.

For example,

get (1, "a", true) |> printf "%s"

prints a.

val iter: 'handlers -> 'p -> unit

Iterates over the elements of the product of type 'p using the handler functions in the product of functions of type 'handlers.

Each handler function must have a type of one of the forms

                 'e -> unit
int           -> 'e -> unit
       string -> 'e -> unit
int -> string -> 'e -> unit

where the type 'e is the type of an element of 'p, the int is the index of the element, and the string is the name of the element.

Only records and single case union types have labeled elements. The handler is chosen by attempting to get an element of one of the above types from the handlers product.

For example,

iter (printf "%s", printf "%1.1f", printf "%d") (1, "x", 2.0)

prints 1x2.0.

val init: 'handlers -> 'p

Creates a value of the given product of type 'p using the handler functions in the product of function and values of type 'handlers.

Each handler function or value must have a type of one of the forms

                 'e
int           -> 'e
       string -> 'e
int -> string -> 'e

where the type 'e is the type of an element of 'p, the int is the index of the element, and the string is the name of the element.

Only records and single case union types have labeled elements. The handler is chosen by attempting to get an element of one of the above types from the handlers product.

For example,

init (sprintf "%d") : string * string * string

returns the tuple ("0", "1", "2").

val fold: 'handlers -> 'p -> 's -> 's

Fold over the elements of the product of type 'p using the handler functions in the product of functions of type 'handlers.

Each handler function must have a type of one of the forms

                 'e -> 's -> 's
int           -> 'e -> 's -> 's
       string -> 'e -> 's -> 's
int -> string -> 'e -> 's -> 's

where 's is the type of the fold state, 'e is the type of an element of 'p, the int is the index of the element, and the string is the name of the element.

Only records and single case union types have labeled elements. The handler is chosen by attempting to get an element of one of the above types from the handlers product.

For example,

iter (sprintf "%s"    >> (+),
      sprintf "%1.1f" >> (+),
      sprintf "%d"    >> (+))
     (1, "x", 2.0)

returns "2.0x1".

[<AutoOpen>]
module Rec =

type RecVal<'t> =

Combination of ref<'t> and Rec<'t>. See also: recVal.

val mutable Rec: 't

This is initially default initialized, but may later be written with a value of type 't via the Rec<'t> base class to tie the knot.

new: (RecVal<'t> -> 't) -> RecVal<'t>

Constructs a new RecVal<'t>, given a function that returns a new value of type 't that delegates to RecVal.Rec, but does not read it immediately. See recVal.

val recVal<'t> : (RecVal<'t> -> 't) -> Rec<'t>

Conveniently creates a RecVal<'t> and returns it as a Rec<'t>.

The given function should delegate to RecVal.Rec, but must not read it immediately. For example, one could define Rec.Fun as follows:

static member Fun () = recVal <| fun r -> fun x -> r.Rec x

Note that the above does not read r.Rec immediately. The following definition

static member Fun () = recVal <| fun r -> r.Rec : _ -> _

reads r.Rec immediately and does not work correctly.

type Rec =

Rules for computing fixed points over products, single case union types (aka newtypes) and functions.

Consider the following toy example:

type Fib () =
  inherit Rules ()
  static member fib (fib: int -> int) : int -> int =
    fun n -> if n < 2 then n else fib (n-1) + fib (n-2)

An attempt to generate<Fib, int -> int> fails: the only rule, namely fib, that could generate int -> int, requires a int -> int, which leads Infers to look for a Rec<int -> int> rule, which fails.

We can make Fib depend on Rec to add a rule for making recursive functions:

type [<Rec>] Fib () =
  inherit Rules ()
  static member fib (fib: int -> int) : int -> int =
    fun n -> if n < 2 then n else fib (n-1) + fib (n-2)

Now generate<Fib, int -> int> returns the desired function.

Of course, the above is very much a toy example. One usually uses Rec to allow Infers to generate functions to manipulate recursive types.

[<AutoOpen>]
module SomeOf =

val someOf<'t> : 't

someOf<'t> attempts to generate a valid value of type 't.

module Zipper =

[<AbstractClass>] 
type Zipper<'w> =

Zipper over type 'w pointing at an unknown type of hole.

[<AbstractClass>] 
and [<AbstractClass>] Zipper<'w, 'h> =

Zipper over type 'w pointing at a hole of type 'h.

Infers.Toys Library Reference

Synopsis

Description