Finmap for record types

Stream: lean4

[Scott Godwin]

I'm trying to implement a simple type theory with finite product types. Finmap looks like exactly what I want to define record types, so I tried:

import Mathlib.Data.Finmap

inductive Ty where
  | nat : Ty
  | prod : Finmap (λ (_ : String) => Ty) → Ty
  | arrow : Ty → Ty → Ty

which causes:

application type mismatch
  Multiset.NodupKeys entries
argument has type
  Multiset _nested.Sigma_2
but function has type
  Multiset ((_ : String) × Ty) → Prop

The error isn't really clear to me what the problem is, so I instead tried pulling it out:

import Mathlib.Data.Finmap

def Map (α β : Type) : Type := Finmap (λ (_ : α) => β)

inductive Ty where
  | nat : Ty
  | prod : Map String Ty → Ty
  | arrow : Ty → Ty → Ty

but this causes:

(kernel) arg #1 of 'Ty.prod' contains a non valid occurrence of the datatypes being declared

which seems to be indicate it fails the positivity check? Is there a way I can use Finmap to do what I want or do I have to roll my own definition?

[Mario Carneiro]

You can only use a very limited set of type wrappers around the type being defined. I recommend using either fixed arity (e.g. a binary product constructor), or functions

[Mario Carneiro]

Here's a way to get a very similar definition to the one you were trying to do using functions instead:

import Mathlib.Data.Finset.Basic

inductive Ty where
  | nat : Ty
  | prod (s : Finset String) : (s → Ty) → Ty
  | arrow : Ty → Ty → Ty

[Scott Godwin]

Thanks, that helps. I was a bit confused by s → Ty, took me a while to figure out there's a CoeSort. Now just need to figure out how I can similarly define tuple expressions considering they're intrinsically typed.