Separation of Concerns: when is it best to disassociate semantics from syntax?

Question

Choices

Typeclasses are brilliant in that they allow us to adjoin extra structure to existing types. Thereby allowing us to defer some design decisions rather than making rushed decision at the time of conception.

On the other hand, in object oriented programming, for example, we are forced to consider what a type needs to do immediately and any additional structure that is apparent, or needed, at a later time would be incorporated into a subtype.

Everything has its purposes. I'm wondering when it would be best to do one or the other, in the context of Agda.

Non-contrived Example

Using the following for n -ary functions s → s → ... → s → t,

Func : ∀ {ℓ} (a : ℕ) (s : Set ℓ) (t : Set ℓ) → Set ℓ
Func zero s t = t
Func (suc a) s t = s → Func a s t

When defining the syntax of a programming language, we might take a type symbol to be a named item that is 'formed' by taking a number of other such named items, and it's meaning is understood by an operation that takes the aforementioned parameters and produces an concrete Agda Set.

record Type₁ : Set₁ where
 constructor cons₁
 field
  name₁      : String
  arity₁     : ℕ
  paramters₁ : Vec Type₁ arity₁
  semantics₁ : Func arity₁ Type₁ Set

open Type₁

So we package the symbol and the interpretation into one type. Alternatively, we can separate the two:

record Type₂ : Set₁ where 
 constructor cons₂
 field
  name₂      : String
  arity₂     : ℕ
  paramters  : Vec Type₂ arity₂

open Type₂ {{...}}

record HasMeaning (t : Type₂) : Set₁ where
  field
    semantics₂ : Func (arity₂ {{t}}) Type₂ Set

open HasMeaning {{...}}

( Note that we needed Type₂ to live in Set₁, even though it really lives in Set, due to using Func above in HasMeaning. )

Which is best and why? In particular, which is better from the point of view of programming and which is better from the view of proving?

Semantics

Say we actually want to do things with our type(symbols), such as interpret them as actual Agda types, then we can do so easily with the first definition:

⟦_⟧₁ : Type₁ → Set 
⟦ cons₁ name₁ 0 [] semantics₁ ⟧₁ = semantics₁
⟦ cons₁ name₁ (suc n) (hd ∷ tl) semantics₁ ⟧₁ = 
     ⟦ cons₁ name₁ n tl (semantics₁ hd) ⟧₁

Nothing clever. If there are no 'parameters' then the semantics-function is necessarily an Agda Set and we're done; otherwise, we feed in the first type parameter to the semantics-function and recurse to obtain a concrete Set.

It's a tad annoying with the second definition since we need to place the typeclass constraint each time we want to use the semantics of a type, which, for me, is a lot!

⟦_⟧₂ : (t : Type₂) {{_ : HasMeaning t}} → Set
⟦ cons₂ name₂ 0 [] ⟧₂ {{s}} = semantics₂ {{s}}
⟦ cons₂ name₂ (suc n) (hd ∷ tl) ⟧₂ {{s}} = 
     ⟦ cons₂ name₂ n tl ⟧₂ 
     {{ record { semantics₂ = semantics₂ {{s}} hd } }}

Even worse, what if we have conflicting semantics instances? Perhaps we want at most one instance, how would we achieve that?

So, for my purposes, it seems the first is best...or not..

Equality

The second definition clearly admits decidable equality, since naturals and strings have decidable equality. However, the first does not due to the interpretation functions. This problem can be sidestepped by saying two type(symbols) are identical precisely when they have identical names, arties, and parameters; irrespective of interpretation:

postulate eq₁-desire : ∀ {n a p S T} → cons₁ n a p S ≡ cons₁ n a p T

Sadly, this does not give us computation and that can be fixed by using trustMe.

Decisions

As far as I can tell, from the above rambling, the first approach along with trustMe is the way to go. However, I'm not terribly comfortable using trustMe ---I know very little about it.

Any advice on which way to go, or any reasons on which approach to follow, would be most appreciated. Thank-you!

Answer 1

I think, first of all you should separate name-arity-semantics part from Type. Since every Type can be coerced to a Set, you can represent semantics as a function from Sets to Set rather than from Types to Set (this is also strictly positive unlike your Type₁). Here is how it looks:

record Atom : Set₁ where
  constructor packAtom
  field
    name      : String
    arity     : ℕ
    semantics : Func arity Set Set

record Type : Set₁ where
  inductive
  constructor packType
  field atom : Atom

  open Atom atom

  field parameters : Vec Type arity

mutual
  ⟦_⟧ : Type -> Set
  ⟦ packType (packAtom n ar sem) ts ⟧ = ⟦ ts ⟧s sem

  ⟦_⟧s : ∀ {ar} -> Vec Type ar -> Func ar Set Set -> Set
  ⟦ []     ⟧s A = A
  ⟦ t ∷ ts ⟧s F = ⟦ ts ⟧s (F ⟦ t ⟧) 

Then your question can be restated as "is there a way to force arity and semantics to be determined by a name?". But Agda doesn't enforce global uniqueness of instances. Moreover, it seems like you want to internalize a meta-theorem "there is a unique semantics for each name", so you can use it from within your code, but that's just too much to want. Could you give an example of why this is required?