[Agda] subset types? refinement types? type synonyms? type abbreviations?

[Ramana Kumar]

Liam, thanks for the quick reply. That may be close to what I want,
but I want a subset of the terms rather than of the types. And
replacing HOLType by HOLTerm in your solution doesn't quite work.

Since my development so far is pretty short, I hope you don't mind my
pasting it here.
At risk of confusion, all the "HOL" prefixes I put in my original
email are dropped.

Also, I am indexing terms by whether or not they are a variable (as
well as by their type); I use that information for the Abs
constructor. As I said before, I'd rather not index by anything if
that's an option.

How can I define Formula?

(any style tips would also be appreciated)

module Hol where

open import Data.String
open import Data.Nat
open import Data.Vec
open import Data.Bool

record TypeOperator : Set where
  field name  : String
        arity : ℕ

data Type : Set where
  TyVar : String -> Type
  TyApp : (op : TypeOperator) -> Vec Type (TypeOperator.arity op) -> Type

fun_tyop : TypeOperator
fun_tyop = record { name = "->"; arity = 2 }
_⇒_     : Type -> Type -> Type
t1 ⇒ t2 = TyApp fun_tyop (t1 ∷ [ t2 ])

bool_tyop : TypeOperator
bool_tyop = record { name = "bool"; arity = 0 }
bool : Type
bool = TyApp bool_tyop []

record Constant : Set where
  field name : String
        type : Type

data Term : {_ : Type} -> {_ : Bool} -> Set where
  Var   : String -> (t : Type) -> Term {t} {true}
  Const : (c : Constant) -> Term {Constant.type c} {false}
  App   : ∀ {x} {y} {b1} {b2} -> Term {x ⇒ y} {b1} -> Term {x} {b2} ->
Term {y} {false}
  Abs   : ∀ {x} {y} {b} -> Term {x} {true} -> Term {y} {b} -> Term {x
⇒ y} {false}

Formula : Bool -> Set
Formula = Term bool

-- data Thm : Formula -> FinSet Formula -> Set where

On Thu, Nov 10, 2011 at 3:19 PM, Liam O'Connor <liamoc at cse.unsw.edu.au> wrote:
> If I understand your question, perhaps something like:
> HOLFormula : Set
> HOLFormula = HOLType BoolT
> Is what you're after?
> This is just a simple type synonym, but it's written like a value
> definition.
> Agda needs no special construct for this (unlike some other theorem provers
> I've used cough isabelle cough)
> --
> Liam O'Connor
>
> On Friday, 11 November 2011 at 2:13 AM, Ramana Kumar wrote:
>
> Suppose I have defined an inductive datatype in Agda representing
> Higher-Order Logic terms, indexed by their type.
> So I have
> data HOLTerm : HOLType -> Set where ...
> Now suppose I want to create a type HOLFormula that picks out the
> terms whose type is boolean.
> (Suppose I have booltype : HOLType in Agda.)
> What are my options? How can I do that?
> I am pretty new to Agda, so it might be a simple question with a simple
> answer.
> Will I be able to use HOLFormulas pretty much the same way as HOLTerms
> (pattern matching on them the same etc.) except I know that their type
> is bool (and am obliged to prove it when I provide one to a function)?
> If that's possible, is there a chance of using similar techniques to
> define HOLTerm in a non-indexed way, but so that it still captures all
> and only the well-typed HOL terms? The reason why I am using an
> indexed type at the moment is that some of the constructors require
> terms coming in with a certain type. For example
> App : forall {x} {y} -> HOLTerm (fun_type x y) -> HOLTerm x -> HOLTerm y
> But if I could define subtypes of HOLTerms mutually with the
> definition of HOLTerms, there would be a chance of avoiding the
> indexing...
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>