Interleaving typechecking and evaluation [Re: [Agda] Recursive Sets / refine vs. load]

Andreas Abel andreas.abel at ifi.lmu.de
Fri Mar 30 15:08:42 CEST 2012

```Hi Thorsten,

I shall make my statement more pecise.  We do not need the concept of
declaration to make this work.

Have

T = Bool -> Set

then define the value

[ |- fix t:T. \x:Bool. case x of
true -> Nat
false -> Sigma (t true) (Vec Bool)
: T ]

The brackets indicate the McBride sheds of not-yet type-checked stuff,
which cannot be evaluated.

The whole value becomes in the first step (recursion)

let rec v = [ t = v : T |- \x:Bool. case x of
true -> Nat
false -> Sigma (t true) (Vec Bool)
: T ]

then

let rec v = \ x -> [ t = v : T, x : Bool |- case x of
true -> Nat
false -> Sigma (t true) (Vec Bool)
: Set ]

then

let rec v = \ x -> case [ t = v : T, x : Bool |- x : Bool ] of
true ->  [ t = v : T, x = true  : Bool |- Nat : Set]
false -> [ t = v : T, x = false : Bool |- Sigma (t true) (Vec
Bool) : Set ]

then

let rec v = \ x -> case x of
true -> Nat
false -> let A = [ t = v : T, x = false : Bool |- t true : Set]
in Sigma A [ (Vec Bool) : A -> Set ]

then

let rec v = \ x -> case x of
true -> Nat
false -> let A = [ t = v : T, x = false : Bool |- t : T]
[ t = v : T, x = false : Bool |- true : Bool ]
in Sigma A [ (Vec Bool) : A -> Set ]
then

let rec v = \ x -> case x of
true -> Nat
false -> let A = v true
in Sigma A [ (Vec Bool) : A -> Set ]

then

let rec v = \ x -> case x of
true -> Nat
false -> let A = case true of
true -> Nat
false -> let A = v true
in Sigma A [ (Vec Bool) : A -> Set ]
in Sigma A [ (Vec Bool) : A -> Set ]

then

let rec v = \ x -> case x of
true -> Nat
false -> let A = Nat
in Sigma A [ (Vec Bool) : A -> Set ]
then

let rec v = \ x -> case x of
true -> Nat
false -> let A = Nat
in Sigma A [ (Vec Bool) : A -> Set ]
then

let rec v = \ x -> case x of
true -> Nat
false -> let A = Nat
in Sigma Nat [ (Vec Bool) : Nat -> Set ]

finally

let rec v = \ x -> case x of
true -> Nat
false -> let A = Nat
in Sigma Nat Vec Bool

Hoorray, type checked!

And we did not peek into boxes during evaluation.

Sharing seems essential.

Hopefully, this was precise enough.

Cheers,
Andreas

On 3/28/12 1:52 PM, Altenkirch Thorsten wrote:
> Could you make this more precise, Andreas?
>
> It seems that the approach using equations also exploits that we define
> everything top-level.
> I don't see how to generalize this in a way which would extend uniformly
> to eliminators appearing
> anywhere. But maybe this is just my limitation...
>
> Cheers,
> Thorsten
>
> On 27/03/2012 21:07, "Andreas Abel"<andreas.abel at ifi.lmu.de>  wrote:
>
>> Well, you could make sense of this, even if thinking it as a case.
>> But then, the boundary between type-checked code that can be evaluated
>> and not-yet-type-checked code is within terms, not only declarations.
>>
>> Cheers,
>> Andreas
>>
>> On Sun, 25 Mar 2012 16:55:36 +0100, Altenkirch Thorsten wrote:
>>> To me pattern matching is just a shorthand for using eliminators such
>>> as case. In this view it is hard to make sense of your suggestion.
>>>
>>> Cheers,
>>> Thorsten
>>>
>>>
>>> On 24 Mar 2012, at 22:13, "Nils Anders Danielsson"<nad at chalmers.se>
>>> wrote:
>>>
>>>> On 2012-03-24 18:12, Brandon Moore wrote:
>>>>> The following definition looks reasonable to me,
>>>>> the type of the hole is reported as ℕ → Set,
>>>>> and refine/give accepts what I've written there,
>>>>> but then typechecking the file fails, saying
>>>>> t true !=<  ℕ of type Set
>>>>
>>>> [...]
>>>>
>>>>> t : Bool → Set
>>>>> t true = ℕ
>>>>> t false = Σ (t true) {!Vec Bool!}
>>>>>
>>>>> Why isn't this definition accepted?
>>>>
>>>> Because (non-mutual) definitions are not unfolded before they have
>>>> been
>>>> type-checked. Unfortunately this does not apply to goals: Agda
>>>> forgets
>>>> that t should not unfold when Vec Bool is type-checked. This is a
>>>> long-standing bug:
>>>>
>>>>
>>>> --
>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>> This message and any attachment are intended solely for the addressee
>>> and may contain confidential information. If you have received this
>>> message in error, please send it back to me, and immediately delete
>>> it.   Please do not use, copy or disclose the information contained
>>> in
>>> this message or in any attachment.  Any views or opinions expressed
>>> by
>>> the author of this email do not necessarily reflect the views of the
>>> University of Nottingham.
>>>
>>> This message has been checked for viruses but the contents of an
>>> attachment
>>> may still contain software viruses which could damage your computer
>>> system:
>>> you are advised to perform your own checks. Email communications with
>>> the
>>> University of Nottingham may be monitored as permitted by UK
>>> legislation.
>>
>> --
>> Andreas Abel<><      Du bist der geliebte Mensch.
>>
>> Theoretical Computer Science, University of Munich
>> http://www.tcs.informatik.uni-muenchen.de/~abel/
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>

--
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/
```