[Agda] Pie in the sky

[Samuel Gélineau]

On 2010-09-20 22:31, Andreas Abel wrote:
> As I heard from Ulf, the main reason why it is not in Agda is that there is
> not a good idea yet how to handle scoping.  Haskell's mistakes should not be
> repeated.

I'm not familiar with those mistakes, but it would be important to
make sure that Benja's proposed feature doesn't have similar scoping
issues, then. And as a matter of fact, I think the proposal does have
issues, although those I have noticed are probably quite different
from Haskell's.

First, it seems that the proposal has a slightly inconsistent naming
scheme. Sometimes the special implicit values are given the same name
as their type, and sometimes their name is an underscore.

Second, the usage examples clearly show that the implicit values are
intended to be listed in the type, but not in the pattern-matching
part of function definitions. According to the current agda scoping
rules, the implicit value should therefore not be in scope inside the
body, and the type checker would thus not be able to look in the
current environment to find a value whose name is the same as the type
of an implicit value it failed to solve.

Third, the fact that an implicit value's name can have spaces in it
means its name cannot appear anywhere a name can normally appear, lest
is be confused for a series of names.

Thus, I think Benja's proposal needs more work, but I stand by my
enthusiasm: this idea has a lot of potential.

---

And now, here is my attempt at fixing the flaws highlighted above. My
version of the proposal is to introduce a new syntax for compound
names, say '(Foo bar), where (Foo bar) is some expression which agda
evaluates to its normal form. Now also introduce the syntax '{Foo
bar}, as a shorthand for {'(Foo bar)}, and the keyword (default). When
(default) is put in a context where a value of type (Foo bar) is
expected, '(Foo bar) is looked up in the current environment, causing
a compile error if none is found.

When an argument of type (Foo bar) is omitted, first behave as if _
was given at this location. If the meta cannot be solved, behave as if
default was given at this location. If this fails too, give a compile
error.

Here is how using this version of the proposal would look like:


-- default can be used both in the type and the body,
-- as long as the appropriate '(T) is in scope.
_$_ : {'(T) : T} → T.carrier default → T.carrier default → T.carrier default
_$_ '{T} x y = T.op default x y

-- there is no need to tag the ord parameter in a special way.
insert : ∀ {X Y} → {ord : Ord X} → X → Y → Map X Y → Map X Y
insert = ...

module Int where
  data Int : Set where ...

  -- this comparison implementation will be used by default for Int...
  '(Ord Int) : Ord Int
  '(Ord Int) = record { ... }

-- ...unless you don't want to.
open import Int hiding ('(Ord Int))

-- the name '(Monad M) really can be used anywhere an ordinary variable
-- name can, as long as Monad and M are in scope.
liftM : ∀ {M A B} → {'(Monad M) : Monad M} → (A -> B) → (M A -> M B)
liftM {M} {'(Monad M) = '(Monad M)} f m = m >>= λ x → return (f x) where
  open Monad default

_/_ : (x y : Rational) → {_ : y /= 0} → Rational
_/_ = ...

-- '{z /= 0} is used for the third argument of _/_.
foo : (x y z : Rational) → {_ : z /= 0} → Rational
foo x y z '{z /= 0} = (x + y) / z

-- instead of having both putStr and hPutStr, as in Haskell,
-- use a single putStr but use stdout as the default Stream.
'(Stream) = stdout
putStr : ∀ {Stream} → String → IO ()
putStr = ...


hoping you like my version of the proposal,
– Samuel