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

[Andreas Abel]

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
>>>
>>> Sent from my iPad
>>>
>>> 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:
>>>>
>>>>    http://code.google.com/p/agda/issues/detail?id=118
>>>>
>>>> --
>>>> /NAD
>>>>
>>>> _______________________________________________
>>>> 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/