Conclusions.lidr 1.92 KB
 Nicola Botta committed Mar 02, 2021 1 2 3 4 5 6 7 8 9 10 11 12 13 14 % -*-Latex-*- %if False > %default total > %auto_implicits off > %access public export %endif \section{Conclusions, outlook} \label{section:conclusions} In dependently typed programming in the context of Martin-Löf type  Nicola Botta committed Mar 08, 2021 15 theories \citep{martinlof1984, nordstrom1990programming}, the problem of  Nicola Botta committed Mar 06, 2021 16 17 how to specify abstract data types for verified generic programming is still not well understood.  Nicola Botta committed Mar 02, 2021 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 % In this work, we have shown that requiring functors to preserve extensional equality of arrows yields abstract data types that are strong enough to support the verification of non-trivial monadic laws and of generic results in domain specific languages for dynamical system and control theory. We have shown that such a minimalist approach can be exploited to derive results that otherwise would require enforcing the relationships between monadic operators -- |pure|, bind, join, Kleisli composition, etc. -- through intensional equalities or, even worse, postulating function extensionality or similar \emph{impossible} specifications. As a consequence we have proposed to carefully distinguish between functors whose associated |map| can be shown to preserve extensional equality (and identity arrows and arrow composition) and functors for which this is not the case. % %(We are working on a characterization theorem relating extensional %equality preservation to traversable functors.) Current work by two of the authors shows that preservation of extensional equality is useful in designing a verified ADT for Applicative functors \citep{mcbride2008applicative} and that all Traversable functors satisfy |mapPresEE|. We conjecture that carefully distinguishing between higher order functions that can be shown to preserve extensional equality and higher order functions for which this is not the case can pay high dividends (in terms of concise and correct generic implementations and avoidance of boilerplate code) also for other abstract data types.