[Agda-dev] A tutorial on inference in Agda

[Roman]

Andreas, thanks a lot for your very helpful comments!

I've fixed the typos and added the acknowledgements section. I'll
incorporate the rest of your feedback once I have some spare time
(this weekend most likely).

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

>  []       ⊛ []       = []

I tried it and can confirm that the unresolved meta goes away. Which
makes perfect sense, I'll reflect this in the document.

Thanks again!

2020-10-26 14:07 GMT+03:00, Andreas Abel <abela at chalmers.se>:
> 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/
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>