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

[Ramana Kumar]

On Thu, Nov 10, 2011 at 9:40 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Hello Ramana,
>
>> 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.
>
> I would not do it like that.  Rather have a separate type of variables,
>
>  data Var : Type -> Set
>
> and then
>
>  data Term : Type -> Set where
>    var : {t : Type} -> Var t -> Term t
>    ...
>    abs : {t u : Type} -> Var t -> Term u -> Term (t => u)
>
> Or even better, use some flavor of nameless term representation.  You see a
> lot of approaches advertized in the later messages of the threat
> "Associativity for free!".

I would like to use named (and typed) variables if possible to keep
close to the ML implementation of terms in, say the HOL theorem
prover. However if that turns out to be too much of a departure from
comfortable idioms in a dependently typed setting I may have to
switch... For the same reason I would rather use a non-indexed type of
terms. I'm curious - whether or not it's desirable - is it actually
possible? I know one could define raw terms then take a subset of it
(although not sure how to concretely do that in Agda), but is it
possible to define well-typed terms all at once without using an
indexed type?

>
>> How can I define Formula?
>
>>
>>
>> Formula : Bool ->  Set
>> Formula = Term bool
>
> I am confused, didn't you just define Formula?  It is a Term of type bool,

But that code fails in Agda. I tried to define it like that and it
wouldn't load. Note that I would want Formula to share the same
constructors as Term.

> that's it.
>
> Cheers,
> Andreas
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>