Type inference for plain data

The context behind this post is that my partner asked me how to implement type inference for plain data structures (e.g. JSON or YAML) which was awfully convenient because this is something I’ve done a couple of times already and there is a pretty elegant trick for this I wanted to share.

Now, normally type inference and unification are a bit tricky to implement in a programming language with functions, but they’re actually fairly simple to implement if all you have to work with is plain data. To illustrate this, I’ll implement and walk through a simple type inference algorithm for JSON-like expressions.

For this post I’ll use the Value type from Haskell’s aeson package, which represents a JSON value¹:

data Value
    = Object (KeyMap Value)  -- { "key₀": value₀, "key₁": value₁, … }
    | Array (Vector Value)   -- [ element₀, element₁, … ]
    | String Text            -- e.g. "example string"
    | Number Scientific      -- e.g. 42.0
    | Bool Bool              -- true or false
    | Null                   -- null

I’ll also introduce a Type datatype to represent the type of a JSON value, which is partially inspired by TypeScript:

import Data.Aeson.KeyMap (KeyMap)

data Type
    = ObjectType (KeyMap Type)  -- { "key₀": type₀, "key₁": type₁, … }
    | ArrayType Type            -- type[]
    | StringType                -- string
    | NumberType                -- number
    | BoolType                  -- boolean
    | Optional Type             -- null | type
    | Never                     -- never, the subtype of all other types
    | Any                       -- any, the supertype of all other types
    deriving (Show)

… and the goal is that we want to implement an infer function that has this type:

import Data.Aeson (Value(..))

infer :: Value -> Type

I want to walk through a few test cases before diving into the implementation, otherwise it might not be clear what the Type constructors are supposed to represent:

>>> -- I'll use the usual `x : T` syntax to denote "`x` has type `T`"
>>> -- I'll also use TypeScript notation for the types

>>> -- "example string" : string
>>> infer (String "example string")
StringType

>>> -- true : boolean
>>> infer (Bool True)
BoolType

>>> -- false : boolean
>>> infer (Bool False)
BoolType

>>> -- 42 : number
>>> infer (Number 42)
NumberType

>>> -- [ 2, 3, 5 ] : number[]
>>> infer (Array [Number 2, Number 3, Number 5])
ArrayType NumberType

>>> -- [ 2, "hello" ] : any[]
>>> -- To keep things simple, we'll differ from TypeScript and not infer
>>> -- a type like (number | string)[].  That's an exercise for the reader.
>>> infer (Array [Number 2, String "hello"])
ArrayType Any

>>> -- [] : never[]
>>> infer (Array [])
ArrayType Never

>>> -- { "key₀": true, "key₁": 42 } : { "key₀": bool, "key₁": number }
>>> infer (Object [("key₀", Bool True), ("key₁", Number 42)])
ObjectType [("key₀", BoolType), ("key₁", NumberType)]

>>> -- [{ "key₀": true }, { "key₁": 42 }] : { "key₀": null | bool, "key₁": null | bool }[]
>>> infer (Array [Object [("key₀", Bool True)], Object [("key₁", Number 42)]]) 
ArrayType (ObjectType (fromList [("key₀",Optional BoolType),("key₀",Optional NumberType)]))

>>> -- null : null | never
>>> infer Null
Optional Never

>>> -- [ null, true ] : (null | boolean)[]
>>> infer (Array [Null, Bool True])
ArrayType (Optional Bool)

Some of those test cases correspond almost 1-to-1 with the implementation of infer, which we can begin to implement:

infer :: Value -> Type
infer (String _) = StringType
infer (Bool _) = BoolType
infer (Number _) = NumberType
infer Null = Optional Never
…

The main two non-trivial cases are the implementation of infer for Objects and Arrays.

We’ll start with Objects since that’s the easier case to infer. To infer the type of an object we infer the type of each field and then collect those field types into the final object type:

infer (Object fields) = ObjectType (fmap infer fields)

The last tricky bit to implement is the case for Arrays. We might start with something like this:

infer (Array elements) = ArrayType ???

… but what goes in the result? This is NOT correct:

infer (Array elements) = ArrayType (fmap infer elements)

… because there can only be a single element type for the whole array. We can infer the type of each element, but if those element types don’t match then we need some way to unify those element types into a single element type representing the entire array. In other words, we need a function with this type:

unify :: Vector Type -> Type

… because if we had such function then we could write:

infer (Array elements) = ArrayType (unify (fmap infer elements))

The trick to doing this is that we need to implement a Monoid instance and Semigroup instance for Type, which is the same as saying that we need to define two functions:

-- The default type `unify` returns if our list is empty
mempty :: Type

-- Unify two types into one
(<>) :: Type -> Type -> Type

… because if we implement those two functions then our unify function becomes … fold!

import Data.Foldable (fold)
import Data.Vector (Vector)

unify :: Vector Type -> Type
unify = fold

The documentation for fold explains how it works:

Given a structure with elements whose type is a Monoid, combine them via the monoid’s (<>) operator.

Laws

There are a few rules we need to be aware of when implementing mempty and (<>) which will help ensure that our implementation of unification is well-behaved.

First, mempty and (<>) must obey the “Monoid laws”, which require that:

-- Left identity
mempty <> x = x

-- Right identity
x <> mempty = x

-- Associativity
x <> (y <> z) = (x <> y) <> z

Second, mempty and (<>) must additionally obey the following unification laws:

• mempty is a subtype of x, for all x
• x <> y is a supertype of both x and y

Unification

mempty is easy to implement since according to the unification laws mempty must be the universal subtype, which is the Never type:

instance Monoid Type where
    mempty = Never

(<>) is the more interesting function to implement, and we’ll start with the easy cases:

instance Semigroup Type where
    StringType <> StringType = StringType
    NumberType <> NumberType = NumberType
    BoolType <> BoolType = BoolType

    …

If we unify any scalar type with itself, we get back the same type. That’s pretty self-explanatory.

The next two cases are also pretty simple:

    Never <> other = other
    other <> Never = other

If we unify the Never type with any other type, then we get the other type because Never is a subtype of every other type.

The next case is slightly more interesting:

    ArrayType left <> ArrayType right = ArrayType (left <> right)

If we unify two array types, then we unify their element types. But what about Optional types?

    Optional left <> Optional right = Optional (left <> right)

    Optional left <> right = Optional (left <> right)
    left <> Optional right = Optional (left <> right)

If we unify two Optional types, then we unify their element types, but we also handle the case where only one or the other type is Optional, too.

The last complex data type is objects, which has the most interesting implementation:

    ObjectType left <> ObjectType right =
        ObjectType (KeyMap.alignWith adapt left right)
      where
        adapt (This (Optional a)) = Optional a
        adapt (That (Optional b)) = Optional b
        adapt (This a) = Optional a
        adapt (That b) = Optional b
        adapt (These a b) = a <> b

You can read that as saying “to unify two objects, unify the types of their respective fields, and if either object has an extra field not present in the other object then wrap the field’s type in Optional”.

Finally, we have the case of last resort:

    _ <> _ = Any

If we try to unify two types that could not unify via the previous rules, then fall back to Any (the supertype of all other types).

This gives us our final program (which I’ll included in its entirety here):

import Data.Aeson (Value(..))
import Data.Aeson.KeyMap (KeyMap)
import Data.Foldable (fold)
import Data.These (These(..))
import Data.Vector (Vector)

import qualified Data.Aeson.KeyMap as KeyMap

data Type
    = ObjectType (KeyMap Type)  -- { "key₀": type₀, "key₁": type₁, … }
    | ArrayType Type            -- type[]
    | StringType                -- string
    | NumberType                -- number
    | BoolType                  -- boolean
    | Optional Type             -- null | type
    | Never                     -- never, the subtype of all other types
    | Any                       -- any, the supertype of all other types
    deriving (Show)

infer :: Value -> Type
infer (String _) = StringType
infer (Bool _) = BoolType
infer (Number _) = NumberType
infer Null = Optional Never
infer (Object fields) = ObjectType (fmap infer fields)
infer (Array elements) = ArrayType (unify (fmap infer elements))

unify :: Vector Type -> Type
unify = fold

instance Monoid Type where
    mempty = Never

instance Semigroup Type where
    StringType <> StringType = StringType
    NumberType <> NumberType = NumberType
    BoolType <> BoolType = BoolType

    Never <> other = other
    other <> Never = other

    ArrayType left <> ArrayType right = ArrayType (left <> right)

    Optional left <> Optional right = Optional (left <> right)

    Optional left <> right = Optional (left <> right)
    left <> Optional right = Optional (left <> right)

    ObjectType left <> ObjectType right =
        ObjectType (KeyMap.alignWith adapt left right)
      where
        adapt (This (Optional a)) = Optional a
        adapt (That (Optional b)) = Optional b
        adapt (This a) = Optional a
        adapt (That b) = Optional b
        adapt (These a b) = a <> b

    _ <> _ = Any

Pretty simple! That’s the complete implementation of type inference and unification.

Unification laws

I mentioned that our implementation should satisfy the Monoid laws and unification laws, so I’ll include some quick proof sketches (albeit not full formal proofs), starting with the unification laws.

Let’s start with the first unification law:

• mempty is the subtype of x, for all x

This is true because we define mempty = Never and Never is the subtype of all other types.

Next, let’s show that the implementation of (<>) satisfies the other unification law:

• x <> y is a super type of both x and y

The first case is:

    StringType <> StringType = StringType

This satisfies the unificaiton law because if we replace both x and y with StringType we get:

• StringType <> StringType is a supertype of both StringType and StringType

… and since StringType <> StringType = StringType that simplifies down to:

• StringType is a supertype of both StringType and StringType

… and every type is a supertype of itself, so this satisfies the unification law.

We’d prove the unification law for the next two cases in the exact same way (just replacing StringType with NumberType or BoolType):

    NumberType <> NumberType = NumberType
    BoolType <> BoolType = BoolType

What about the next case:

    Never <> other = other

Well, if we take our unification law and replace x with Never and replace y with other we get:

• Never <> other is a supertype of Never and other

… and since Never <> other = other that simplifies to:

• other is a supertype of Never and other

… which is true because:

• other is a supertype of Never (because Never is the universal subtype)
• other is a supertype of other (because every type is a supertype of itself)

We’d prove the next case in the exact same way (just swapping Never and other):

    other <> Never = other

For the next case:

    ArrayType left <> ArrayType right = ArrayType (left <> right)

The unification law becomes:

• ArrayType (left <> right) is a supertype of both ArrayType left and ArrayType right

… which is true because ArrayType is covariant and by induction left <> right is a supertype of both left and right.

We’d prove the first case for Optional in the exact same way (just replace Array with Optional):

    Optional left <> Optional right = Optional (left <> right)

The next case for Optional is more interesting:

    Optional left <> right = Optional (left <> right)

Here the unification law would be:

• Optional (left <> right) is a supertype of Optional left and right

… which is true because:

• Optional (left <> right) is a supertype of Optional left

  This is true because Optional is covariant and left <> right is a supertype of left

• Optional (left <> right) is a supertype of right

  This is true because:

  • Optional (left <> right) is a supertype of Optional right
  • Optional right is a supertype of right
  • Therefore, by transitivity, Optional (left <> right) is a supertype of right

We’d prove the next case in the same, just switching left and right:

    left <> Optional right = Optional (left <> right)

The case for objects is the most interesting case:

    ObjectType left <> ObjectType right =
        ObjectType (KeyMap.alignWith adapt left right)
      where
        adapt (This (Optional a)) = Optional a
        adapt (That (Optional b)) = Optional b
        adapt (This a) = Optional a
        adapt (That b) = Optional b
        adapt (These a b) = a <> b

I won’t prove this case as formally, but the basic idea is that this is true because a record type (A) is a supertype of another record type (B) if and only if:

• for each field k they share in common, A.k is a supertype of B.k
• for each field k present only in A, A.k is a supertype of Optional Never
• there are no fields present only in B

… and given that definition of record subtyping then the above implementation satisfies the unification law.

Monoid laws

The first two Monoid laws are trivial to prove:

mempty <> x = x

x <> mempty = x

… because we defined:

    mempty = Never

… and if we replace mempty with Never in those laws:

Never <> x = x
x <> Never = x

… that is literally what our code defines (except replacing x with other):

    Never <> other = other
    other <> Never = other

The last law, associativity, is pretty tedious to prove in full:

(x <> y) <> z = x <> (y <> z)

… but I’ll do a few cases to show how the basic gist of how the proof works.

First, the associativity law is easy to prove for the case where any of x, y, or z is Never. For example, if x = Never, then we get:

(Never <> y) <> z = Never <> (y <> z)

-- Never <> other = other
y <> z = y <> z

… which is true. The other two cases for y = Never and z = Never are equally simple to prove.

Associativity is also easy to prove when any of x, y, or z is Any. For example, if x = Any, then we get:

(Any <> y) <> z = Any <> (y <> z)

-- Any <> other = other
Any <> z = Any

-- Any <> other = other
Any = Any

… which is true. The other two cases for y = Any and Z = Any are equally simple to prove.

Now we can prove associativity if any of x, y or z is StringType. The reason why is that these are the only relevant cases in the implementation of unification for StringType:

StringType <> StringType = StringType

StringType <> Never = StringType
Never <> StringType = StringType

StringType <> _ = Any
_ <> StringType = Any

… but we already proved associativity for all cases involving a Never, so we don’t need to consider the second case, which simplifies things down to:

StringType <> StringType = StringType

StringType <> _ = Any
_ <> StringType = Any

That means, that there are only seven cases we need to consider to prove the associativity laws if at least one of x, y, and z is StringType (using _ below to denote “any type other than StringType):

-- true: both sides evaluate to StringType
(StringType <> StringType) <> StringType = StringType <> (StringType <> StringType)

-- all other cases below are also true: they all evaluate to `Any`
(StringType <> StringType) <> _          = StringType <> (StringType <> _         )
(StringType <> _         ) <> StringType = StringType <> (_          <> StringType)
(StringType <> _         ) <> _          = StringType <> (_          <> _         )
(_          <> StringType) <> StringType = _          <> (StringType <> StringType)
(_          <> StringType) <> _          = _          <> (StringType <> _         )
(_          <> _         ) <> StringType = _          <> (_          <> StringType)

We can similarly prove associativity for all cases involving at least one NumberType or BoolType.

The proof for ArrayType is almost the same as the proof for StringType/NumberType/BoolType. The only relevant cases are:

ArrayType left <> ArrayType right = ArrayType (left <> right)

ArrayType left <> Never = ArrayType
Never <> ArrayType right = ArrayType

ArrayType left <> _ = Any
_ <> ArrayType right = Any

Just like before, we can ignore the case where either argument is Never because we already proved associativity for that. That just leaves:

ArrayType left <> ArrayType right = ArrayType (left <> right)

ArrayType left <> _ = Any
_ <> ArrayType right = Any

Just like before, there are only seven cases we have to prove (using _ below to denote “any type other than ArrayType):

ArrayType x <> (ArrayType y <> ArrayType z) = (ArrayType x <> ArrayType y) <> ArrayType z
-- … simplifies to:
ArrayType (x <> (y <> z)) = ArrayType ((x <> y) <> z)
-- … which is true because unification of the element types is associative

-- all other cases below are also true: they all evaluate to `Any`
(ArrayType x <> ArrayType y) <> _           = ArrayType x <> (ArrayType y <> _          )
(ArrayType x <> _          ) <> ArrayType z = ArrayType x <> (_           <> ArrayType z)
(ArrayType x <> _          ) <> _           = ArrayType x <> (_           <> _          )
(_           <> ArrayType y) <> ArrayType z = _           <> (ArrayType y <> ArrayType z)
(_           <> ArrayType y) <> _           = _           <> (ArrayType y <> _          )
(_           <> _          ) <> ArrayType z = _           <> (_           <> ArrayType z)

The proofs for the Optional and Object cases are longer and more laborious so I’ll omit them. They’re an exercise for the reader because I am LAZY.

---

1. I’ve inlined all the type synonyms and removed strictness annotations, for clarity↩︎

Prompt chaining reimagined with type inference

At work I’ve been researching how to improve the ergonomics of prompt engineering and I wanted to share and open source some of what I’ve done. This initial post is about how I’ve been experimenting with using bidirectional type inference to streamline prompt chaining.

“Prompt chaining” is a prompt engineering technique that splits a larger task/prompt into multiple smaller tasks/prompts which are chained together using code. For example, instead of prompting a model to generate a poem in one prompt like this:

Write a poem based off this idea:

${idea}

… by following this process:

• First think through the form, stanza count, lines per stanza, and rhyme scheme
• Then choose a poetic style (tone, voice, and literary devices) based on the poem’s form
• Then write a complete poem based on that plan

… you can split it into smaller prompts, like this:

structure prompt:

Plan the structure of a new poem based on this idea

${idea}

Describe its form, stanza count, lines per stanza, and rhyme scheme

style prompt:

Given this poem structure:

• Form: ${structure.form}
• Stanzas: ${structure.stanzaCount}
• Lines per stanza: ${structure.linesPerStanza}
• Rhyme scheme: ${structure.rhymeScheme}

Choose a poetic style: tone, voice, and literary devices to emphasize

poem prompt:

Write a complete poem based on this idea:

${idea}

Structure:

• Form: ${structure.form}
• Stanzas: ${structure.stanzaCount}
• Lines per stanza: ${structure.linesPerStanza}
• Rhyme scheme: ${structure.rhymeScheme}

Style:

• Tone: ${style.stone}
• Voice: ${style.voice}
• Literary Devices: ${style.literaryDevices}

Why might you want to do this?

• to improve the quality of the results

  Models perform better when working on more constrained subproblems. Splitting a larger prompt into smaller prompts helps the model stay focused at each step.

• to introspect intermediate results

  This comes in handy when you want to log, validate, or correct intermediate results.

• to perform actions in between prompts

  You might want to take the output of one prompt, use that to call some tool, then use the output of that tool to decide what the next prompt should be, which you can’t do with a single prompt.

In other words, prompt chaining unlocks greater accuracy, control, and flexibility for prompt engineering.

The problem

The main issue with prompt chaining is that it is a huge pain in the ass; if you start do anything a little bit complicated you need to start using structured outputs (i.e. JSON), which adds a whole lot of boilerplate to the process:

• you have to define the schema for each intermediate step of the process

  You typically do this by defining your data model in your host programming language (e.g. a Pydantic model in Python) or directly defining your JSON schema

• You have to instruct the model to produce JSON and explain the shape of the expected output

• (Depending on the framework) you have to decode the JSON into your data model

For small prompt chaining pipelines this isn’t too hard, but it starts to get annoying to define all these schemas when you scale this up to more sophisticated prompt chaining pipelines.

So as a thought experiment I wanted to create a research prototype that handled all of that for you so that you didn’t need to specify any schemas at all. In other words I wanted to build a programming language that harnessed bidirectional type inference to perform schema inference for prompts with structured JSON outputs.

Example

I’ll cut to the case by showing the above prompt chain written as a program in this language:

let concatSep =
      https://raw.githubusercontent.com/Gabriella439/grace/refs/heads/main/prelude/text/concatSep.ffg

let lines = concatSep "\n"

let generatePoem idea =
        let structure = prompt
                { model: "gpt-4o"
                , text: lines
                    [ "Plan the structure of a new poem based on this idea:"
                    , ""
                    , idea
                    , ""
                    , "Describe its form, stanza count, lines per stanza, and rhyme scheme."
                    ]
                }

        let renderedStructure = lines
                [ "- Form: " + structure.form
                , "- Stanzas: " + Real/show (structure.stanzaCount : Integer)
                , "- Lines per stanza: " + Real/show (structure.linesPerStanza : Integer)
                , "- Rhyme scheme: " + structure.rhymeScheme
                ]

        let style = prompt
                { model: "gpt-4o"
                , text: lines
                    [ "Given this poem structure:"
                    , renderedStructure
                    , ""
                    , "Choose a poetic style: tone, voice, and literary devices to emphasize."
                    ]
                }

        let renderedStyle = lines
                [ "- Tone: " + style.tone
                , "- Voice: " + style.voice
                , "- Literary Devices: " + concatSep ", " style.literaryDevices
                ]

        let poem : Text = prompt
                { model: "gpt-4o"
                , text: lines
                    [ "Write a complete poem based on this idea:"
                    , ""
                    , idea
                    , ""
                    , "Structure:"
                    , renderedStructure
                    , ""
                    , "Style:"
                    , renderedStyle
                    ]
                }

        in { structure: structure, style: style, poem: poem }

in  generatePoem "The stillness of early morning"

The above prompt chain is a real program in a research programming language named Fall-from-Grace (or “Grace” for short). Specifically, this is implemented in a branch of the language that adds a magic prompt keyword that works like in the above example.

If you run the above example, you might get an output like this:

{
  "structure": {
    "form": "Free verse with a sprinkle of rhyme",
    "linesPerStanza": 4,
    "rhymeScheme": "ABCB",
    "stanzaCount": 5
  },
  "style": {
    "literaryDevices": [
      "imagery",
      "alliteration",
      "personification",
      "enjambment"
    ],
    "tone": "nostalgic",
    "voice": "reflective"
  },
  "poem": "### The Stillness of Early Morning\n\n**I**  \nIn the gentle rise of dawn's embrace,  \nA whisper of winds through sleepy skies,  \nThe world lies suspended in an echo  \nOf yesterday's dreams, reluctantly saying goodbye.\n\n**II**  \nSoft orange light graces fields of dew,  \nCradling tenacious tendrils of the past.  \nMorning breathes upon the waiting world  \nWith promises that this serenity will last.\n\n**III**  \nWaves of silence surge across the meadow,  \nNature's symphony gently cradles rest.  \nA chorus of leaves sings its soft refrain,  \nComforted by morning's tender caress.\n\n**IV**  \nThe silence dips to caress weary trees,  \nWhose branches waltz to whispers soft and slow.  \nEach tendril holds close the morning's intention,  \nBefore the day's demands, the chaos, start to show.\n\n**V**  \nEarly rays dance upon a tranquil sea,  \nA canvas painted through a dreamy haze.  \nTime sits by, savoring the gentle hush,  \nAs the world awakens, stirs, and finally plays."
}

… and if you’re curious what the formatted poem looks like:

The Stillness of Early Morning

I
In the gentle rise of dawn’s embrace,
A whisper of winds through sleepy skies,
The world lies suspended in an echo
Of yesterday’s dreams, reluctantly saying goodbye.

II
Soft orange light graces fields of dew,
Cradling tenacious tendrils of the past.
Morning breathes upon the waiting world
With promises that this serenity will last.

III
Waves of silence surge across the meadow,
Nature’s symphony gently cradles rest.
A chorus of leaves sings its soft refrain,
Comforted by morning’s tender caress.

IV
The silence dips to caress weary trees,
Whose branches waltz to whispers soft and slow.
Each tendril holds close the morning’s intention,
Before the day’s demands, the chaos, start to show.

V
Early rays dance upon a tranquil sea,
A canvas painted through a dreamy haze.
Time sits by, savoring the gentle hush,
As the world awakens, stirs, and finally plays.

Type inference

The sample Grace program hardly specifies any types (mainly the final expected type for the poem: Text). The reason this works is because Grace supports bidirectional type inference, which means that Grace can work backwards from how intermediate results are used to infer their schemas.

I’ll illustrate this with a contrived Grace example:

let numbers = prompt{ text: "Give me two numbers" }

in  { x: numbers.x
    , y: numbers.y
    , sum: numbers.x + numbers.y : Integer
    }

… which might produce an output like this:

$ grace interpret ./numbers.ffg

{ "x": 7, "y": 14, "sum": 21 }

When Grace analyzes this program the type checker works backwards from this expression:

numbers.x + numbers.y : Integer

… and reasons about it like this:

• the addition produces an Integer, therefore numbers.x and numbers.y must also be Integers

• therefore numbers is a record with two fields, x and y, both of which are Integers

  … or using Grace syntax, the inferred type of numbers is: { x: Integer, y: Integer }

• therefore the output of the prompt command must have the same type

… and then Grace generates a JSON schema for the prompt which looks like this:

{ "type": "object",
  "properties": {
    "x": { "type": "integer" },
    "y": { "type": "integer" }
  },
  "required": [ "x", "y" ],
  "additionalProperties": false
}

Of course, you can specify types if you want (and they’re more lightweight than schemas in traditional prompt chaining frameworks). For example:

$ grace repl
>>> prompt{ text: "Give me a first and last name" } : { first: Text, last: Text }
{ "first": "Emily", "last": "Johnson" }
>>> prompt{ text: "Give me a list of names" } : List Text
[ "Alice"
, "Bob"
, "Charlie"
, "Diana"
, "Ethan"
, "Fiona"
, "George"
, "Hannah"
, "Isaac"
, "Jack"
]

However in our original example we don’t need to specify intermediate types because when the type-checker sees this code:

let structure = prompt
        { model: "gpt-4o"
        , text: lines
            [ "Plan the structure of a new poem based on this idea:"
            , ""
            , idea
            , ""
            , "Describe its form, stanza count, lines per stanza, and rhyme scheme."
            ]
        }

let renderedStructure = lines
        [ "- Form: " + structure.form
        , "- Stanzas: " + Real/show (structure.stanzaCount : Integer)
        , "- Lines per stanza: " + Real/show (structure.linesPerStanza : Integer)
        , "- Rhyme scheme: " + structure.rhymeScheme
        ]

… the compiler can reason backwards from how the structure value is used to infer that the JSON schema for the prompt needs to be:

{ "type": "object",
  "properties": {
    "form": { "type": "string" },
    "stanzaCount": { "type": "integer" },
    "linesPerStanza": { "type": "integer" },
    "rhymeScheme": { "type": "string" }
  },
  "required": [
    "form",
    "stanzaCount",
    "linesPerStanza",
    "rhymeScheme"
    ],
  "additionalProperties": false
}

Tool use

Grace also supports generating sum types (a.k.a. tagged unions), and you can imagine using this to subsume traditional tool use frameworks.

For example, consider this Grace program:

let concatSep = https://raw.githubusercontent.com/Gabriella439/grace/refs/heads/main/prelude/text/concatSep.ffg

let call = merge
      { HttpRequest: \x -> "curl " + x.url
      , ShellCommand: \x -> concatSep " " ([ x.executable ] + x.arguments)
      }

in  List/map call (prompt{ text: "Call some tools" })

This doesn’t actually run any tools (I haven’t added any callable tools to my work-in-progress branch yet), but just renders the tool use as a string for now:

$ grace interpret ./tools.ffg

[ "curl https://api.example.com/data", "ls -l -a" ]

However, the idea is that you can model a tool as a sum type with one constructor per callable tool, and in the above example the type checker infers that the sum type representing one tool call is:

< HttpRequest: { url: Text }
| ShellCommand: { executable: Text, arguments: List Text }
>

… so the inferred type of call is:

call : < HttpRequest: …, ShellCommand: … > -> Text

… but since we List/map the call function over the output of the prompt the type checker infers that the prompt needs to generate a List of tool calls:

prompt{ text: "Call some tools" } : List < HttpRequest: …, ShellCommand: … >

… and then Grace does some magic under the hood to convert that type to the equivalent JSON schema.

What’s particularly neat about this example is that the prompt is so incredibly bare (“Call some tools”) because all the information the model needs is present in the schema.

Schema-driven prompting

We can explore this idea of using the schema to drive the prompt instead of prose using an example like this:

prompt{ text: "Generate some characters for a story", model: "gpt-4o" }
  : List
    { "The character's name": Text
    , "The most memorable thing about the character": Text
    , "The character's personal arc": Text
    }

[ { "The character's name": "Aveline Thatcher"
  , "The character's personal arc":
      "Aveline starts as a skeptical journalist who doubts the stories of mythical creatures. Over time, she becomes a firm believer, risking her career to uncover the truth and protect these creatures."
  , "The most memorable thing about the character":
      "The intricate tattoo of a phoenix on her forearm that seems to glow when she discovers hidden truths."
  }
, { "The character's name": "Kelan Frost"
  , "The character's personal arc":
      "A former rogue alchemist who turns hero after he inadvertently creates a dangerous substance. Driven by guilt, Kelan seeks redemption by finding an antidote and saving his village."
  , "The most memorable thing about the character":
      "His iridescent blue eyes that seem to see into one's soul, a side effect of his alchemical experiments."
  }
, { "The character's name": "Luciana Blair"
  , "The character's personal arc":
      "Luciana is a reclusive artist who initially fears the world outside her home. After a mysterious vision rejuvenates her, she sets out on a journey of self-discovery, ultimately finding both her voice and courage."
  , "The most memorable thing about the character":
      "Her ability to paint scenes before they happen, which she attributes to the visions she sees in her dreams."
  }
, { "The character's name": "Ezra Hartman"
  , "The character's personal arc":
      "Once a charismatic but self-centered lawyer, Ezra is confronted with a moral crisis that forces him to reevaluate his values. He chooses a path of integrity, becoming an advocate for justice."
  , "The most memorable thing about the character":
      "His perfectly tailored suits that slowly become more casual, symbolizing his transformation and shifting priorities."
  }
, { "The character's name": "Seraphine Mora"
  , "The character's personal arc":
      "Seraphine is a young music prodigy who loses her hearing after an accident. Battling despair, she learns to embrace a new way of 'hearing' music through vibrations and her other senses."
  , "The most memorable thing about the character":
      "The ethereal way she 'dances' with the music, using her entire body to express each note's emotion."
  }
]

Grace is a superset of JSON and since JSON supports arbitrary field names so does Grace! Field names in Grace support arbitrary capitalization, punctuation, and whitespace as long as you quote them, and we can use the field names to “smuggle” the description of each field into the schema.

Conclusion

Hopefully this gives you some idea of why I’ve begun to think of prompt chaining as a programming languages problem. Type inference is just the beginning and I think it is possible to use a domain-specific programming language not just to simplify the code but to ultimately unlock greater reasoning power.

I’m going to continue to use Grace as a research vehicle for prompt chaining but my LLM-enabled branch of Grace (like Grace itself) is not really intended to be used in production and I created it mainly as a proof-of-concept for where I’d like prompt chaining frameworks to go. If I do end up eventually productionizing this research I will create a proper fork with its own name and the whole works.