[Agda-dev] A tutorial on inference in Agda

[Andreas Abel]

Hello Roman,

 > I wrote a painfully long tutorial on the way Agda does unification:

Indeed, ;-) took my whole morning to read.

But this is a very nice and comprehensive tutorial, thanks for writing 
all this up!

I learned a few new tricks/perspectives, which I hope to remember e.g.:
- _∘
- dependent K
- Promote

Below there are some comments on your text.

Cheers,
Andreas


# Section "Implicit arguments":

Exceptions to eager implicit argument insertion are so called "aliases" 
(x = e) like

   _∘ = _∘_

which you mention in the "Basics" section.  Here, we insert implicit 
arguments lazily (because they would **always** be unsolved otherwise, 
by absence of a type signature).

You could mention this exception here in the text.


# Arguments of data types / Comparison to Haskell

I couldn't read this relative sentence at my usual speed (limits my 
parser stack) so I gave up on trying to comprehend it:

 > because it elaborates to
 > ...
 > (due to eager insertion of implicits) and the fact that there's a 
variable of type ℕ bound in the current scope (regardless of whether 
it's bound explicitly or implicitly) does not have any effect on how 
implicits get resolved in the body of the definition as metavariable 
resolution does not come up with instantiations for metavariables at 
random by looking at the local or global scope, it only determines what 
instantiations are bound to be by solving unification problems that 
arise during type checking.


# Under the hood / Example 3

Small inaccuracy in

 > List _A (this time the type of the result that listId returns) also 
gets unified with the expected type, which is ℕ -> ℕ,

rather: List (ℕ -> ℕ)


# Nicer notation

Remark:

 > We'll denote "X uniquely determines Y" (the notation comes from the 
bidirectional typechecking discipline) as X ⇉ Y. So List A ⇉ A.

Without ever having dived deeply into the technical details, this 
matches my intuition about Haskell's FunctionalDependencies. 
Unfortunately, Haskell's type constructors are not injective in that 
sense, due to some weird corner cases involving infinite type 
expressions.  I always bump my head into this weakness of 
FunctionalDependencies, they just defy my intuition.


# Type functions

 > Therefore, F A (where F is a bound variable) uniquely determines 
neither F nor A, i.e. F A !⇉ F , A.

Here you could point to the difference between first-order and higher 
unification.  The user often expects that Agda performs first-order 
unification here (this is why Coq chose to facilitate also first-order 
unification, leading to non-unique solutions).  Agda, however, only does 
higher-unification, and there are many solutions (as you explained).

Future research could improve on unification via an analysis in which 
situation the chosen solution does not matter.  (However, I never got 
around to do this research.)

The example you give is such an instance: It does not matter how we 
solve _F _A = List Nat, because the solutions of _F and _A can never 
flow out of the expression

   fId _F _A (1 ∷ 2 ∷ []) : _F _A


# Reduction

Formatting problem in

 > headᵥ⁺-wrong is a contrived example, but this problem can arise in 
real cases, for example consider a naive attempt to define 
thereversefunction overVec` using an accumulator,


# Pattern Matching

 > weird definition of the plus operator

This is the accumulator-version of plus, I seem to recall it was used in 
the standard library (at least at some point) in connection with reverse 
for vectors (or something else).

 > So we have the following rule of thumb: whenever the type of function 
h mentions function f at the type level, every argument that gets 
pattern matched on in f (including any internal function calls) should 
be made explicit in h and every other argument can be left implicit 
(there are a few exceptions to this rule, which we'll consider below, 
but it applies in most cases).

+1.  My experience confirms this rule.


# Constructor/argument-headed functions / Example 2: polyvariadic 
zipWith: list-based

 > Omitting an argument results in metas not being resolved in the 
version of Agda that I'm using

Might be worthwhile stating the version.

 > _ : zipWithN _+_ (1 ∷ᵥ 2 ∷ᵥ 3 ∷ᵥ []ᵥ) _ ≡ (5 ∷ᵥ 7 ∷ᵥ 9 ∷ᵥ []ᵥ)
 > _ = refl

 > This is something that I can't explain

The remaining meta is (recent master)

   _xs_2474 : Vec ℕ 0

It might stem from the laziness of `[] ⊛_`

   _⊛_ : ∀ {n} → Vec (A → B) n → Vec A n → Vec B n
   []       ⊛ _        = []
   (f ∷ fs) ⊛ (x ∷ xs) = f x ∷ (fs ⊛ xs)

Maybe if you make it stricter, constructor-headedness kicks in.

   []       ⊛ []       = []

This could be an issue to consider for the library maintainers.


# (Close to the end)

typo: dependenty-typed


On 2020-10-26 03:03, Roman wrote:
> Hi folks,
> 
> I wrote a painfully long tutorial on the way Agda does unification:
> https://htmlpreview.github.io/?https://github.com/effectfully/unification-in-agda/blob/master/UnificationInAgda.html
> 
> It targets the users of Agda, so it doesn't cover advanced topics like
> higher-order unification.
> 
> I'd like to hear your opinion before I share the link with a general
> audience. Is there something horribly wrong there? What can be
> improved? Are there any missing parts of the unification engine that
> would be nice to cover? Is the tutorial readable in general? Any kind
> of feedback would be highly appreciated.
> 
> Please don't share the link publicly yet.
> 
> BTW, I generate such HTMLs in an absolutely awful way. Does Agda
> support generating an HTML page (with all the coloring) from an Agda
> file when that file contains warnings, unresolved metas etc? And is
> there a flag to make Agda accept ill-typed code, show a warning and
> proceed with type checking? And color ill-typed code in red or
> something, like unresolved metas are colored in yellow.
> 
> Best regards.
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
> 

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/