`copilot-core`: Add documentation for `updateField` describing how (and why) to implement it

[RyanGlScott]

Copilot 3.20 added support for struct updates via the new UpdateField operation. One slightly non-obvious aspect of UpdateField is that copilot-interpreter doesn't support interpreting it unless you make sure to implement the updateField method in the Struct instance of any struct that whose field you update. For example, here is a naïve attempt at interpreting a Copilot specification involving a struct update:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
module Main (main) where

import Language.Copilot

data S = S
  { unS :: Field "unS" Word32
  }

instance Struct S where
  typeName _ = "s"
  toValues s = [Value typeOf (unS s)]

instance Typed S where
  typeOf = Struct (S (Field 0))

spec :: Spec
spec = do
  let externS :: Stream S
      externS = extern "extern_s" (Just [S (Field 0)])

      example :: Stream Word32
      example = (externS ## unS =: 42) # unS

  trigger "example" (example == example) [arg externS, arg example]

main :: IO ()
main = interpret 1 spec

This will fail with:

$ runghc UpdateFieldInterpreterFail.hs 
UpdateFieldInterpreterFail.hs: Field updates not supported for this type.
CallStack (from HasCallStack):
  error, called at src/Copilot/Core/Type.hs:64:17 in copilot-core-3.20-inplace:Copilot.Core.Type

To make this work, you need to implement updateField in the Struct S instance. Here is an example of how to do that:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Main (main) where

import Data.Proxy (Proxy(..))
import Data.Type.Equality (TestEquality(..), (:~:)(..))
import GHC.TypeLits (sameSymbol)
import qualified Prelude as P

import Language.Copilot

data S = S
  { unS :: Field "unS" Word32
  }

instance Struct S where
  typeName _ = "s"
  toValues s = [Value typeOf (unS s)]
  updateField s (Value fieldTy (field :: Field s a)) =
    case (sameSymbol (Proxy @s) (Proxy @"unS"), testEquality fieldTy Word32) of
      (Just Refl, Just Refl) -> s { unS = field }
      _ -> error $ "Unexpected field: " P.++ show field

instance Typed S where
  typeOf = Struct (S (Field 0))

spec :: Spec
spec = do
  let externS :: Stream S
      externS = extern "extern_s" (Just [S (Field 0)])

      example :: Stream Word32
      example = (externS ## unS =: 42) # unS

  trigger "example" (example == example) [arg externS, arg example]

main :: IO ()
main = interpret 1 spec

$ runghc UpdateFieldInterpreter.hs 
example:     
(<unS:0>,42)

The catch here is that I only knew how to do this because I was involved in the design of the updateField method. Unfortunately, there are currently no Haddocks for updateField itself, nor is there any kind of indication in the Copilot documentation that you would need to implement updateField like shown above in order to make copilot-interpreter work. Given how subtle this process is, I think there should be some kind of tutorial in the documentation about how to do this.

It might also be helpful if the Field updates not supported for this type error message indicated that you need to implement updateField.

[RyanGlScott]

Perhaps the best way to tutorialize this would be to extend the existing struct-related examples in the Copilot repo (e.g., this one and this one) to demonstrate how to implement updateField for them.

(Note that if we implement the ideas in https://github.com/Copilot-Language/copilot/discussions/540, we might also want to update the examples to automatically derive updateField implementations rather than implement them explicitly. If that happens, it might also be worth having separate examples that show how to implement updateField manually rather than using deriving.)

[ivanperez-keera]

Description

Copilot 3.20 added support for struct updates via a new UpdateField operation.

For struct updates to be usable in the interpreter, the creator of the spec must implement the updateField method in the Struct instance of any structs that need to be updated. The implementation of that function is non-trivial; we must include examples and documentation to help users understand how to write those definitions.

Type

• Feature: include additional documentation to aid understanding.

Additional context

None.

Requester

• Ryan Scott (Galois)

Method to check presence of bug

Not applicable (not a bug).

Expected result

There is documentation available to help users understand how to write those instances.

Desired result

There is documentation available to help users understand how to write those instances.

Proposed solution

Add an example that includes several structs that are updated.

Add haddocs for the type class documenting the implementation of the operation, possibly pointing to the example in the repository if the explanation is too long.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 4.1.

Fix assigned to: @RyanGlScott .

[RyanGlScott]

Implementor: Solution implemented, review requested.