<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>The need for dependent types arises because in most cases, we need to describe exactly what a function does, and other type systems are not sufficient.</div><div>For example the function g could be implemented by randomly selecting true or false per int number.</div><div><br></div><div>A more concrete example is agda's Defn(1) definition. There, many of the Maybes depend on the current stage of the computation. The comments play the role of telling the programmer what to expect. <br></div><div>In many cases , comments are missing, or are wrong because you forget to update them. Moreover, to understand the comments, you need to understand the order of the computation. In other words, <br></div><div>you need to learn many parts of the agda code , to simply use a data structure. This type of programming cannot scale. It can only work for a very small group of people, and for a very small code base.<br></div><div><br></div><div>With a refinement of a protocol, I actually mean the refinement as is described in TLA+(2). The arguments are the same as in the previous case. The difference is that now , the group of people that change parts of the protocol / the application <br></div><div>are so many that it is impossible to coordinate them, you might not even know they exist.<br></div><div><br></div><div>On another note, there are very important positive results if we only use the type to determine if a function is correct. Developers are free to use different implementation and this induces an evolutionary process similar to organisms. <br></div><div>Mutations of a protein can exist as long as the functionality remains the same.(3)<br></div><div><br></div><div>(1) : <a href="https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Monad/Base.hs#L1656">https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Monad/Base.hs#L1656</a></div><div>(2) : <a href="https://lamport.azurewebsites.net/tla/tla.html">https://lamport.azurewebsites.net/tla/tla.html</a></div><div>(3) : <a href="http://hal.elte.hu/fij/r/b/dsc/Hartwell.pdf">http://hal.elte.hu/fij/r/b/dsc/Hartwell.pdf</a><br></div></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jan 18, 2019 at 5:42 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Fri, 2019-01-18 at 16:43 +0200, Apostolis Xekoukoulotakis wrote:<br>
> I use agda as a programming language. So the computational path is the<br>
> part of the program that will be executed.<br>
> <br>
> <br>
> For me , agda will help to decentralize the development of software.<br>
> If the types describe a function accurately enough, one can replace<br>
> one implementation with another without the need to coordinate with<br>
> the other developers. <br>
> <br>
> In fact, each developer only needs to know the type and nothing about<br>
> the other parts of the software.<br>
> <br>
> <br>
> Now, if we extend this idea to the development of network protocols,<br>
> we can have an abstract protocol, and developers refining parts of it.<br>
> In that way, we have the concurrent evolution of network protocols<br>
> without the need for a coordination mechanism which in this case , it<br>
> is very difficult to have.<br>
> <br>
> <br>
> I do not see any other way to do this . So for me , agda is<br>
> indispensable .<br>
<br>
<br>
<br>
I do not know any about network protocols. To "refine a part of an<br>
abstract protocol" (whatever this might mean), the developer, may be,<br>
needs be given a specification of the properties of the arguments and of<br>
the properties of the function to be programmed. Is this so?<br>
Suppose, one writes this function in Haskell, and writes so that the<br>
function to satisfy the given specification. And where are dependent<br>
types?<br>
<br>
--<br>
SM<br>
<br>
<br>
</blockquote></div>