[Agda] `where' in type

[Andreas Abel]

Hello Serge,

On 31.08.12 7:53 PM, Serge D. Mechveliani wrote:
> People,
> I have a question about the code
>
>    record CommutativeRing2 c l : Set (suc (max c l))
>      where
>      open CommutativeRing
>      field
>        commutativeRing : CommutativeRing c l
>        fromInt         : Integer -> Carrier commutativeRing
>        divMb           : (Carr -> Carr -> Carr)
>                          where
>                          Carr = Carrier commutativeRing

As in Haskell, 'where' is only allowed on the level of declarations, 
i.e., (x where x = 5) + 3  is a parse error.

And a type signature like 'divMb : ...' (which is a declaration), cannot 
have 'where' clauses.

Your solutions are both good ones.

Cheers
Andreas

>
> (the math symbols are replaced, in order to make this e-mail
> readable:   max := \lub,  Integer := \bz).
>
> This is under  Agda-2.3.0.1 + lib-0.6,
> and it relies on the Algebra part of Standard library:  uses
> CommutativeRing.
>
> The Doc sais that a  record field type  my depend on other field values,
> and I use this in the declarations for  fromInt, divMb.
> Hence, one has a hope that `let' and `where' are allowed in such a
> dependency.
> But this declaration for  divMb  causes  Parse error  -- at `where'.
>
> Replacing it with
>                    divMb : (let Carr = Carrier commutativeRing
>                             in  Carr -> Carr -> Carr)
> makes it compiled.
>
> Why 'where' is not so lucky here as `let' ?
>
> Apart of the `where' question:
> currently I think that the best is the following approach with multiple
> `field' parts.
>
>    record CommutativeRing2 c l : Set ...  where
>      field
>        commutativeRing : CommutativeRing c l
>
>      Carr : Set _
>      Carr = CommutativeRing.Carrier commutativeRing
>
>      field
>        fromInt : Integer -> Carr
>        divMb   : Carr -> Carr -> Maybe Carr
>        isCommutativeRing2 : ...
>
> It is compiled, and I hope that this code is reliable
> (its idea is to avoid copying operation names from a superclass).
>
> Thanks,
>
> ------
> Sergei
> _______________________________________________
> 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/