[Agda] constructor-headed functions to Set

[Andreas Abel]

Hi Brandon,

On 7/13/11 7:13 AM, Brandon Moore wrote:
> I was hoping to use the handling of "constructor-headed functions"to make it possible to write functions whose return type is
> computed from implicit arguments (without always explicitly
> supplying the arguments).
>
> It seems to work if the body of a definition is just the
> function with a computed return type, but
> not if it's applied to any additional arguments
> (which correspond to computed arrows).
>
> module test where
> open import Data.Nat
>
> data T : Set where A : T → T ; R : T
>
> tsem : T → Set
> tsem R = ℕ
> tsem (A t) = ℕ → tsem t
>
> f : (t : T) → tsem t
> f R = 0
> f (A x) = λ _ → f x
>
> test1 : ℕ → ℕ → ℕ
> test1 = f _ -- inferred
>
> test2 : ℕ
> test2 = f _ 1 2 -- not inferred

Mmh, something must have been done, otherwise you would not have gotten 
yellow, but red underlining.

Funnily

   f _ R

also only gives yellow (even though there is no solution), while

   A (f _)

gives an error.

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/