[Agda] First-Class Type Issue

[Jesper Cockx]

Hi Philippe,

You should probably split directly on `x` in the left-hand side instead:

getStringOrInt : (x : Bool) → StringOrInt x
getStringOrInt true = 94
getStringOrInt false = "Ninety four"

or use `case_return_of_` as suggested by Ulf. However, there is a trick
that I'm quite fond of that you can use to make it work even with the
non-dependent `case_of_`:

data Is {ℓ} {A : Set ℓ} : A → Set ℓ where
  ⌊_⌋ : (x : A) → Is x

getStringOrInt : (x : Bool) → StringOrInt x
getStringOrInt x = case ⌊ x ⌋ of λ where
  ⌊ true  ⌋ → 94
  ⌊ false ⌋ → "Ninety Four"

The reason this works is that by using the `Is` datatype, Agda keeps the
connection between the first argument of the `case_of_` and the original
`x`, so when you case split in the `λ where` Agda also refines the original
argument `x` (actually Agda treats both of them as the same variable).

-- Jesper

On Thu, Apr 16, 2020 at 9:26 AM Ulf Norell <ulf.norell at gmail.com> wrote:

> The problem is that the `case_of_` function is non-dependent (the type of
> the branches cannot depend of the value you case on).
> You can use `case_return_of_` instead if you need a dependent match:
>
> getStringOrInt : (x : Bool) → StringOrInt x
> getStringOrInt x = case x return StringOrInt of λ where
>   true → 94
>   false → "Ninety Four"
>
> However, the "correct" way to write the function is
>
> getStringOrInt : (x : Bool) → StringOrInt x
> getStringOrInt true = 94
> getStringOrInt false = "Ninety Four"
>
> / Ulf
>
> On Thu, Apr 16, 2020 at 8:35 AM Philippe de Rochambeau <phiroc at free.fr>
> wrote:
>
>> Hello,
>>
>> when I load the following module,
>>
>> open import Agda.Builtin.Bool
>> open import Agda.Builtin.Nat
>> open import Agda.Builtin.String
>> open import Function using (case_of_)
>>
>> StringOrInt : (x : Bool) → Set
>> StringOrInt x  = case x of λ where
>>     true → Nat
>>     false → String
>>
>> getStringOrInt : (x : Bool) → StringOrInt x
>> getStringOrInt x = case x of λ where
>>   true → 94
>>   false → "Ninety Four"
>>
>>
>> … I get this error message:
>>
>> String != Nat
>> when checking that the expression "Ninety Four" has type Nat
>>
>> Do lambdas only return one data type (in this case, Nat)?
>>
>> Cheers,
>>
>> Philippe
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200416/01c764ff/attachment.html>