The Coq mailing list

["Roly Perera" <roly.perera AT dynamicaspects.org>]

Hi,

I'm afraid this is a bit of a newbie question (with regard both to
Coq, and to dependent types), so if this is not the best forum, my
apologies.  I've been lurking for 6 months or so, and I do see the
occasional newbie post, so I'm hoping I'm not too off target.  (If I
am, any pointers to a more appropriate forum would be welcome.)

I'm trying to define an inductive type that captures the term syntax
of a typed first-order programming language, assuming a fixed set of
types (lowercase "type" from now on meaning a type in my language, not
a Coq Type).

I'm trying to model terms via an inductive type which is indexed by a
type (for now I'm ignoring contexts and variables; one problem at a
time!).  Functions in my language take multiple arguments, so I want
App to be a family of constructors indexed by a list of argument
types.  There will be a function context at some point providing these
signatures, but again, I'm keeping things simple for now.  The idea is
that I can only apply App to a list of terms of the appropriate types.

I can define a dependently typed constructor with a fixed arity
(constructor App2), but I can't see how to create one with variable
arity (constructor App).  I've read Chapter 8 of Adam Chlipala's draft
book (great stuff btw), and I assume heterogenous lists are the key.
I'm fairly comfortable that I understand how the fhlist and fhget
definitions work (I'm not using fhget, but I've included it for
completeness), but I having spent a day or so on it, I can't see how
to make it work.  The code I've attached represents my first naive
attempt.

I get the feeling that what I actually need to do is define my App
constructor in terms of a function from fmember to terms, but the
problem seems to be instantiating term with the right type whilst
keeping the inductive type well-formed (i.e. avoiding 'Non strictly
positive occurrence of "term"').

Any help with this would be greatly appreciated, and apologies again
if this would've been better posted elsewhere.

many thanks,
Roly Perera
-------------------------

Require Import List.

(* Heterogeneous lists. *)
Section fhlist.

Variable A: Type.

Variable B: A -> Type.

Fixpoint fhlist (ls : list A): Type :=
    match ls with
        | nil => unit
        | a :: ls' => (B a * fhlist ls')%type
    end.

Variable a: A.

Fixpoint fmember (ls: list A): Type :=
    match ls with
        | nil => Empty_set
        | a' :: ls' => ((a' = a) + fmember ls')%type
    end.

Fixpoint fhget (ls: list A): fhlist ls -> fmember ls -> B a :=
    match ls return fhlist ls -> fmember ls -> B a with
        | nil =>
            fun _ i => match i with end
        | _ :: ls' =>
            fun hls i =>
                match i with
                    | inl p =>
                        match p with
                            | refl_equal => fst hls
                        end
                    | inr i' => fhget ls' (snd hls) i'
                end
    end.

End fhlist.

(* Fixed set of types. *)
Parameter type: Set.

(* Give myself a type to play with. *)
Parameter Unit: type.

(* Terms are indexed by types. *)
Inductive term: type -> Type :=
    (* Vars are of type Unit for now *)
    | Var: term Unit
    (* Fixed arity: imagine this is an application of a function of
type a -> b -> c *)
    | App2 (a b c: type): term a -> term b -> term c
    (* Variable arity *)
    | App (ls: list type) (c: type): fhlist type term ls -> term c.

Attachment: ToCoqList.v
Description: Binary data