Problems.lagda.rst 17.3 KB
Newer Older
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
..
  ::
  {-# OPTIONS --no-positivity-check --allow-unsolved-metas --rewriting #-}

  module 05-open.Problems where

    open import Data.Product
    open import Data.Nat
    open import Data.List renaming (_++_ to _++L_)
    open import Data.Vec

    open import Relation.Binary.PropositionalEquality

================================================================
Open problems
================================================================

In this course, we have seen that there may be such a thing as
"dependently-typed programming" after all. We saw that it can be:

  - effectufl                     (lecture 1)
  - correct-by-construction       (lecture 2)
  - structurally recursive or not (lecture 3)
  - generic                       (lecture 4)

And it is not just "as good as" languages of the ML family: it enables
genuinely novel and interesting forms of programming.


However, some would argue that programming with dependent type is
unbearably difficult (watch out for disgruntled Coq users). They may
not be absolutely right but perhaps not absolutely wrong either. For
instance, we never had to perform a type cast along a propositional
equality: this is too good to be true. In this last lecture, we
explain why we were able to write these programs so elegantly, we
dissect a few *bad* programs and highlight some very *ugly* (or
impossible) ones.

This time, we shall not try to come to a conclusion: we are touching
upon research questions, only the future will tell whether the AI
robot take over the planet will be programmed with Haskell type
families, C++ template, or ANSI C.

************************************************
The Good
************************************************

We review a few, salient definitions of each lecture. For the
definitions I had to come up with myself or had to reconstruct from a
paper, I provide an estimate of the time it took me to find the
"right" definition (Conor McBride talks about the act of "engineering
coincidences"). This measure must be interpreted in relative terms as
I am, after all, only a moderately clever person with only one PhD
(whose topic was on programming in the inductive fragment of type
theory).

-----------------------------------------
Lecture 0: The Evolution of a Typechecker
-----------------------------------------

The tricky definition is the typechecker itself

.. code-block:: agda

  _?__ : (Γ : context)(T : type)(t : term )  Γ [  ]-view T  t
  _?_  : (Γ : context)(t : term )  Γ [  ]-view t 

that uses ``_[_]-view_`` to ensure that the type-checking or
type-failing derivation produced corresponds to the original term
through the forgetful function ``_``:

.. code-block:: agda

  data _[_]-view_ (Γ : context)(d : dir) : Dir d  Set where
    yes :  {T} (Δ : Γ [ d ] T)    Γ [ d ]-view  Δ 
    no  :  {T} (¬Δ : Γ [ d ] T)   Γ [ d ]-view  ¬Δ 

The trick is to notice that not only is the function ``_`` injective
but it is also merely mapping each **constructor** of the source
datatype to a constructor of the target datatype. Therefore, as we
pattern match on derivations, the type becomes more precise by
revealing a constructor and therefore the forgetful function
mechanically unfolds. If the forgetful map was recursively non
trivial, it would have been another story.


**Estimated time:** It took me about 3 weeks of full-time work to
converge on the final implementation of the type-checker. I initially
thought that I could exploit a monad-generic implementation of the
type-checker to use it for type-directed parsing & pretty-printing but
this was incompatible with the dependently-typed implementation for
which it is not clear how to write it monadically, let alone
monad-generically.

-----------------------------------------
Lecture 1: Effects
-----------------------------------------

The programs we wrote were simply typed so we had it
easy. Nonetheless, we were not able to write the generic definition of
the free monad, which would be::


    data Free (F : Set  Set)(X : Set) : Set where
         return : X  Free F X
         op : F (Free F X)  Free F X

because the positivity-checker would reject this definition: ``F``
provides no guarantee that it will use ``Free F X`` in a
strictly-positive position. This is one of those instances were
relying exclusively on oracles as a way of introducing definitions
impedes compositionality. We have seen in Lecture 4 that it could be
addressed by reflecting inductive types in the type theory itself.

-----------------------------------------
Lecture 2: Indices
-----------------------------------------

Good news, using inductive families for typing ``sprintf`` seems to
qualify as `industrial-strength
<https://ocaml.org/meetings/ocaml/2013/proposals/formats-as-gadts.pdf>`_,
being faster and safer that the untyped alternative.

The expression and machine code are indexed by a type-level tag, which
is almost literally transferred by the compiler

.. code-block:: agda

    compile :  {T σ}  exp T  code σ (T  σ)

If significantly distinct types were used on either side of the
compiler, a non-trivial translation function would be necessary to
state the type of the compiler

.. code-block:: agda

    compile :  {T σ}  exp T  code σ (non-trivial T σ)

which would probably make for a few sleepless nights and type-casting
proofs.

The difficulty of the normalization-by-evaluation program is mostly
conceptual: to deal with binders, one must construct the right model,
which was an issue for category theorists before being one for
dependently-typed programmers.

As part of this exercise, we saw a structural definition of
substitution: this is a folklore trick (that I learned from Conor
McBride), meaning that we can assume that countless hours were spent
by the first person that tried implementing it. Note that it is not a
particularly efficient implementation.

**Estimated time:** It took me about 2 days of full-time work, mostly
studying the literature, to extract the right abstractions to write
the normalization-by-evaluation program. However, dependent types were
instrumental in forcing me to identify these abstractions: in a
simply-typed setting, there is no incentive to do this effort (or one
end up doing pure category theory).

-----------------------------------------
Lecture 3: Recursion
-----------------------------------------

The representation of terms for the MGU relies once again on the
folkore representation of well-scoped terms.

The recursion scheme justifying the proof search was found and
explained by McBride. This is indeed hard work but that needs to be
done anyway. It could be done in a proof-irrelevant manner (using an
accessibility predicate to justify the general-recursive definition,
for example) or in a proof-relevant manner (which is what we did
here).

**Estimated time:** It took me about 5 days of full-time work to
translate the ideas set forward in McBride's Djinn Monotonic into a
workable implementation. Knowing which datatype to define (it is given
by the paper) and the overall recursion scheme is but one small step:
writing a (correct) implementation handling ordered formuli was far
from trivial. For instance, the straightforward zipper is gone,
replaced by a head-scratching search procedure.

-----------------------------------------
Lecture 4: Generic programming
-----------------------------------------

Programming with algebraic structures was made possible by the
availability of instance arguments (ie. type-classes) in
Agda. However, not all objects lend themselves to being
instances. Attaching structures to (inductive) type formers works like
a charm, since the unifier can rely on a concrete object (the type
former) to drive the instance search.

Attaching structure to a compute type did not work at all. For
instance, I was not able to define any (useful) instance for the
functor ``Hyper Fs``::

    Hyper : List (Set → Set) → Set → Set
    Hyper [] A = A
    Hyper (F ∷ Fs) A = Hyper Fs (F A)

As a poor man's alternative, I reified the identity and composition of
functors as inductive type formers::

    data Id (A : Set) : Set where
      I : A  Id A

    data Seq (G : Set  Set)(F : Set  Set)(A : Set) : Set where
      S : F (G A)  Seq G F A

and attached structure to those: when ``Hyper`` computes, it will
reveal a chain of ``Seq``, potentially closed by an ``Id``, all of
which have the structures wwe are interested in. However, this is not
a silver bullet: on ``Hyper Fs``, with ``Fs`` a quantified variable,
we cannot access any of its structure. We cannot rely on ad-hoc
polymorphism and must manually instantiate the dictionaries.

Also, the paper becomes really interesting in Section 6, in which
alignment between matrices of different dimensions is automatically
computed through the following (simplified) type family:

.. code-block:: guess

   instance Alignable (F  Fs) (F  Gs) where
     (...)
   instance Alignable [] (F  Fs) where
     (...)

From a type-theoretic point of view, the first instance is
meaningless: what does it mean for ``F : Set  Set`` to be "equal" on
both sides? Equality of functions is notoriously ill-behaved in type
theory. I therefore stopped right before Section 6, retreating from a
doomed attempt: the very definition of ``hyper`` as ``List (Set 
Set)`` was already an admission of defeat.

The definition of the ``Desc`` was suspiciously redundant: the sum
product (``_`+_``) codes could have been simulated by ``Π Bool λ {
true  _ ; false  _ }``. However, the former encoding enables a
purely first-order implementation (as an inductively-defined sum)
whereas the latter involves a function type. First, intensional
equality is not well-behaved (understand: useless) on functions, hence
a general tendency to avoid them at all cost. Second, having sums
allows us to levitate the description of descriptions as a purely
first-order object (no function lying around).

-----------------------------------------
Other examples
-----------------------------------------

The Mathcomp library defines `tuples
<https://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.tuple.html>`_,
which are equivalent to our very own vector. However, rather than
defining an inductive family, a tuple of size ``n`` is implemented as
"a list whose length is n". Crucially, the constraint that the length
is equal to n does **not** use propositional equality but decidable
equality over natural numbers:

.. code-block:: coq

    Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.

`Hedberg theorem <https://doi.org/10.1017/S0956796898003153>`_ tells
us that this implies that two tuples are equal if and only if they
package the same list (irrespectively of the proof that established
that these lists are of the right size). This is not an issue in
Vanilla Agda, for which all proofs of equality are equal ("uniqueness
of identity proofs", UIP). It is in Coq or in Agda with the flag
"--without-k".

Aside from allowing us to avoid relying on UIP, this style also
enables the definition of operations on vectors (concatenation,
reversal, etc.) to directly re-use the existing operations on lists:
one just need to prove that the constraints on lengths are respected.

************************************************
The Bad
************************************************

Gibbons definition of hyper-matrices is given as a (nested) datatype::

    data Hyper' (A : Set) : List (Set → Set) → Set where
      Scalar : A → Hyper' A []
      Prism  :  {F Fs}  Hyper' (F A) Fs → Hyper' A (F  Fs)

Once again, this definition would not be manageable in type theory
because it implicitly introduces propositional equality to enforce the
constraint ``Hyper A (F  Fs)`` in the target of the Prism
constructor, which is meaningless for the function ``F``.

Sometimes, even apparently good definitions, such as the pervasive
vectors, are behaving frustratingly. In each of the following
examples, we shall give a working definition with lists and a
computationally-equivalent but non-working version on vectors. The
point is not that the desired functionality *cannot* be implemented
(most of the time, one can rewrite them to side-step the problem) but
rather that a "morally correct" definition or property is forbidden.

The first example is a failure of compositionality, first between two functions::

    module NCons-List (A : Set) where

      ncons :   A  List A  List A
      ncons zero a vs = vs
      ncons (suc m) a vs = a  ncons m a vs

      nseq :   A  List A
      nseq m a = ncons m a []

    module NCons-Vec (A : Set) where

      ncons :  {n} (m : )  A  Vec A n  Vec A (m + n)
      ncons zero a vs = vs
      ncons (suc m) a vs = a  ncons m a vs

      nseq : (m : )  A  Vec A m
      nseq m a = {!ncons m a []!}
      -- m + zero != m of type ℕ
      -- when checking that the expression ncons m a [] has type Vec A m

and, second, between a single (recursive) function::

    module RCons-List (A : Set) where

      _++r_ :  {A : Set} List A  List A  List A
      [] ++r ys = ys
      (x  xs) ++r ys = xs ++r (x  ys)

    module RCons-Vec (A : Set) where

      _++r_ :  {A : Set}{m n}  Vec A m  Vec A n  Vec A (n + m)
      [] ++r ys = {!ys!}
      -- .n != .n + 0 of type ℕ
      -- when checking that the expression ys has type Vec .A (.n + 0)
      (x  xs) ++r ys = {!xs ++r (x ∷ ys)!}
      -- suc (.n + .n) != .n₁ + suc .n of type ℕ
      -- when checking that the expression xs ++r (x  ys) has type Vec .A (.n + suc .n)

This sort of annoyance also happens when stating properties::

    module Cats-List (A : Set) where
      cats0 :  (v : List A)  v ++L []  v
      cats0 [] = refl
      cats0 (x  v) rewrite cats0 v = refl

    module Cats-Vec (A : Set) where

      cats0 :  {n} (v : Vec A n)  v ++ []  {!v!}
                         -- n != n + zero of type ℕ
                         -- when checking that the expression v has type Vec A (n + zero)
      cats0 = {!!}


which means that some proofs are themselves impossible to do
compositionally since the necessary lemmas are simply not
expressible::

    module Rcons-List (A : Set) where

      rcons : List A  A  List A
      rcons [] a = a  []
      rcons (x  xs) a = x  rcons xs a

      last' : (a : A) → List A → A
      last' a [] = a
      last' _ (a ∷ xs) = last' a xs

      last-rcons :  x s z  last' x (rcons s z) ≡ z
      last-rcons x s z = trans (cong (last' x) (cat1 s z)) (last-cat x s (z  []))
        where postulate
                last-cat :  x (s : List A)(s : List A)  last' x (s₁ ++L s₂) ≡ last' (last' x s₁) s₂
                cat1 : ∀ s z → rcons s z ≡ s ++L (z ∷ [])

    module Rcons-Vec (A : Set) where

      rcons : ∀ {n} → Vec A n → A → Vec A (suc n)
      rcons [] a = a ∷ []
      rcons (x ∷ xs) a = x ∷ rcons xs a

      last' :  {n}  (a : A)  Vec A n  A
      last' a [] = a
      last' _ (a  xs) = last' a xs

      postulate
         last-cat : ∀ {m n} x (s₁ : Vec A m)(s₂ : Vec A n) → last' x (s ++ s)  last' (last' x s) s
         cat1 :  {n} (s : Vec A n) z  rcons s z  {!s ++ (z ∷ [])!}
           -- n + suc zero != suc n of type ℕ
           -- when checking that the expression s ++ z  [] has type Vec A (suc n)

      last-rcons :  {n} x (s : Vec A n) z  last' x (rcons s z) ≡ z
      last-rcons {n} x s z = trans {!cong (last' {suc n / n + 1}) ?!} (last-cat x s (z ∷ []))
         -- Heterogeneous equality necessary

An elegant solution (due to `Conor McBride
<http://strictlypositive.org/thesis.pdf>`_) to the problem of stating
and using the above equalities consists in generalizing slightly the
definition of equality so that it becomes **heterogeneous**::

    data __ {A : Set} (x : A) : {B : Set}  B  Set where
      refl : x  x

However, we are still at a loss to write programs such as ``nseq`` or
``_++r_`` in a compositional, proof-free manner.

************************************************
The Ugly
************************************************

Nested datatypes, such as::

    data Bush (A : Set) : Set where
      leaf : A  Bush A
      node : Bush (A × A)  Bush A

    size :  {A}  Bush A  
    size (leaf x) = 1
    size (node b) = let n = size b in n + n

are slightly suspicious in the sense that the constructors are
actually encoding the *size* of the container, the constructor
``leaf`` containing a tuple whose shape is determined by the previous
``node`` constructors. First, programming with such a definition is
not going to be pleasant. Second, to encode structural properties, we
have a better tool at hand: indices and inductive families!


Addressing the second point, one could write::

    data Bush' (A : Set)(n : ℕ) : Set where
      leaf : Vec A n → Bush' A n
      node : Bush' A (n + n) → Bush' A n


Addressing the first point, one realizes that Peano numbers are not
the right fit for indexing this structure::

    data Bin : Set where
      #0 : Bin
      #1 : Bin  Bin

    to : Bin  
    to #0 = 1
    to (#1 n) = let x = to n in x + x

    data Bush'' (A : Set) : Bin  Set where
      leaf : A  Bush'' A #0
      node :  {n}  Bush'' A n  Bush'' A n  Bush'' A (#1 n)



.. Local Variables:
.. mode: agda2
.. End: