{"id":274981,"date":"2016-02-25T23:41:02","date_gmt":"2016-02-25T20:41:02","guid":{"rendered":"http:\/\/savepearlharbor.com\/?p=274981"},"modified":"-0001-11-30T00:00:00","modified_gmt":"-0001-11-29T21:00:00","slug":"","status":"publish","type":"post","link":"https:\/\/savepearlharbor.com\/?p=274981","title":{"rendered":"\u0428\u0430\u0431\u043b\u043e\u043d \u043f\u0440\u043e\u0435\u043a\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f View \u0432 \u044f\u0437\u044b\u043a\u0430\u0445 \u0441 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438"},"content":{"rendered":"<p>       <img decoding=\"async\" src=\"https:\/\/habrastorage.org\/files\/0e0\/67b\/a24\/0e067ba244494c62b8f4941c4898ba60.jpg\"\/><\/p>\n<p>  \u0428\u0430\u0431\u043b\u043e\u043d\u044b \u043f\u0440\u043e\u0435\u043a\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f! \u0412\u043f\u0435\u0440\u0432\u044b\u0435 \u044f \u0443\u0437\u043d\u0430\u043b \u043e \u043d\u0438\u0445 \u043d\u0430 \u043a\u0443\u0440\u0441\u0435 Software Design, \u043a\u043e\u0433\u0434\u0430 \u0443\u0447\u0438\u043b\u0441\u044f \u0432 \u043c\u0430\u0433\u0438\u0441\u0442\u0440\u0430\u0442\u0443\u0440\u0435 \u0410\u043a\u0430\u0434\u0435\u043c\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0443\u043d\u0438\u0432\u0435\u0440\u0441\u0438\u0442\u0435\u0442\u0430. \u041c\u044b \u043f\u0438\u0441\u0430\u043b\u0438 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u043d\u0430 Java \u0441 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u0448\u0430\u0431\u043b\u043e\u043d\u043e\u0432. \u0421 \u0442\u0435\u0445 \u043f\u043e\u0440 \u044d\u0442\u043e \u0441\u043b\u043e\u0432\u043e\u0441\u043e\u0447\u0435\u0442\u0430\u043d\u0438\u0435 \u0430\u0441\u0441\u043e\u0446\u0438\u0438\u0440\u0443\u0435\u0442\u0441\u044f \u0443 \u043c\u0435\u043d\u044f \u0441 \u0447\u0435\u043c-\u0442\u043e \u0442\u0430\u043a\u0438\u043c \u041e\u041e\u041f\u0448\u043d\u044b\u043c. \u041e\u0434\u043d\u0430\u043a\u043e, \u0440\u0430\u0437\u0431\u0438\u0440\u0430\u044f\u0441\u044c \u0441 \u044f\u0437\u044b\u043a\u043e\u043c Agda, \u044f \u043d\u0430\u0442\u043a\u043d\u0443\u043b\u0441\u044f \u043d\u0430 \u0441\u0442\u0430\u0442\u044c\u044e The Power Of Pi, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0440\u0430\u0441\u0441\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442 \u043f\u0440\u043e \u0448\u0430\u0431\u043b\u043e\u043d\u044b \u043f\u0440\u043e\u0435\u043a\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0432 \u044f\u0437\u044b\u043a\u0430\u0445 \u0441 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438!<\/p>\n<p>  \u0412 \u044d\u0442\u043e\u043c \u043f\u043e\u0441\u0442\u0435 \u044f \u0445\u043e\u0447\u0443 \u0440\u0430\u0441\u0441\u043a\u0430\u0437\u0430\u0442\u044c \u043e\u0431 \u043e\u0434\u043d\u043e\u043c \u0438\u0437 \u044d\u0442\u0438\u0445 \u0448\u0430\u0431\u043b\u043e\u043d\u043e\u0432, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f View. \u0421 \u0435\u0433\u043e \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043c\u043e\u0436\u043d\u043e \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u044b\u0432\u0430\u0442\u044c \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u0438\u0435 \u043f\u0440\u0430\u0432\u0438\u043b\u0430 pattern matching&#8217;a. \u0415\u0441\u043b\u0438 \u0432\u0430\u043c \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u043e, \u0447\u0442\u043e \u044d\u0442\u043e \u0437\u0430 \u0448\u0430\u0431\u043b\u043e\u043d, \u0447\u0442\u043e \u0442\u0430\u043a\u043e\u0435 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u0438\u0439 pattern matching, \u043a\u0430\u043a\u043e\u0432\u044b \u043e\u0441\u043e\u0431\u0435\u043d\u043d\u043e\u0441\u0442\u0438 pattern matching&#8217;\u0430 \u0432 \u044f\u0437\u044b\u043a\u0430\u0445 \u0441 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438, \u0438 \u0432\u044b \u0437\u043d\u0430\u043a\u043e\u043c\u044b \u0441 \u043a\u0430\u043a\u0438\u043c-\u043d\u0438\u0431\u0443\u0434\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u044b\u043c \u044f\u0437\u044b\u043a\u043e\u043c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441\u043e \u0441\u0442\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0442\u0438\u043f\u0438\u0437\u0430\u0446\u0438\u0435\u0439 (Haskell, Scala, Ocaml, F#) \u2014 \u0434\u043e\u0431\u0440\u043e \u043f\u043e\u0436\u0430\u043b\u043e\u0432\u0430\u0442\u044c \u043f\u043e\u0434 \u043a\u0430\u0442!<a name=\"habracut\"><\/a><\/p>\n<h1>Views \u0438 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u0438\u0439 pattern matching<\/h1>\n<p>  \u0414\u043b\u044f \u043d\u0430\u0447\u0430\u043b\u0430 \u0440\u0430\u0437\u0431\u0435\u0440\u0451\u043c\u0441\u044f, \u0447\u0442\u043e \u0442\u0430\u043a\u043e\u0435 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u0438\u0439 pattern matching. \u041f\u0443\u0441\u0442\u044c \u043c\u044b \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u043c \u0441 \u043a\u0430\u043a\u0438\u043c-\u043d\u0438\u0431\u0443\u0434\u044c \u0441\u043f\u0438\u0441\u043a\u043e\u043c <i>xs<\/i> \u0438 \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u043c \u043d\u0430 \u043d\u0451\u043c pattern matching:  <\/p>\n<pre><code class=\"scala\">match xs with    [] -&gt; ...   (y : ys) -&gt; ... <\/code><\/pre>\n<p>  \u0417\u0434\u0435\u0441\u044c \u043c\u044b \u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043d\u0430 <i>xs<\/i> \u043b\u0438\u0431\u043e \u043a\u0430\u043a \u043d\u0430 \u043f\u0443\u0441\u0442\u043e\u0439 \u0441\u043f\u0438\u0441\u043e\u043a, \u043b\u0438\u0431\u043e \u043a\u0430\u043a \u043d\u0430 \u0441\u043f\u0438\u0441\u043e\u043a, \u0441\u043e\u0441\u0442\u043e\u044f\u0449\u0438\u0439 \u0438\u0437 \u0433\u043e\u043b\u043e\u0432\u043d\u043e\u0433\u043e \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u0430 \u0438 \u043f\u0440\u0438\u043f\u0438\u0441\u0430\u043d\u043d\u044b\u0439 \u043a \u043d\u0435\u043c\u0443 \u0441\u043f\u0438\u0441\u043a\u0430. \u041d\u043e \u0447\u0442\u043e \u0435\u0441\u043b\u0438 \u043c\u044b \u0445\u043e\u0442\u0438\u043c \u043f\u043e\u0441\u043c\u043e\u0442\u0440\u0435\u0442\u044c \u043d\u0430 <i>xs<\/i>, \u0441\u043a\u0430\u0436\u0435\u043c, \u043a\u0430\u043a \u043d\u0430 \u0441\u043f\u0438\u0441\u043e\u043a, \u0441\u043e\u0441\u0442\u043e\u044f\u0449\u0438\u0439 \u0438\u0437 \u043a\u043e\u043d\u043a\u0430\u0442\u0435\u043d\u0430\u0446\u0438\u0438 \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u0434\u0432\u0443\u0445 \u0441\u043f\u0438\u0441\u043a\u043e\u0432 <i>ys<\/i> \u0438 <i>zs<\/i>? \u0427\u0442\u043e-\u0442\u043e \u0432\u0440\u043e\u0434\u0435  <\/p>\n<pre><code class=\"scala\">match xs with   [] -&gt; ...   (ys ++ zs) -&gt; ... <\/code><\/pre>\n<p>  \u0418\u043d\u044b\u043c\u0438 \u0441\u043b\u043e\u0432\u0430\u043c\u0438, \u043d\u0430\u043c \u0445\u043e\u0447\u0435\u0442\u0441\u044f \u0432\u043b\u0438\u044f\u0442\u044c \u043d\u0430 \u0442\u043e, \u043a\u0430\u043a \u0438\u043c\u0435\u043d\u043d\u043e \u0431\u0443\u0434\u0435\u0442 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0442\u044c\u0441\u044f \u0441\u0442\u0440\u0443\u043a\u0442\u0443\u0440\u0430 \u0434\u0430\u043d\u043d\u044b\u0445 \u0432 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 pattern matching&#8217;a. \u042d\u0442\u043e \u043c\u044b \u0438 \u0431\u0443\u0434\u0435\u043c \u043d\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u0438\u043c pattern matching&#8217;\u043e\u043c.<\/p>\n<p>  \u041f\u043e \u0445\u043e\u0434\u0443 \u0441\u0442\u0430\u0442\u044c\u0438, \u043d\u0430\u0448\u0435\u0439 \u0446\u0435\u043b\u044c\u044e \u0431\u0443\u0434\u0435\u0442 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u043e\u0433\u043e pattern matching&#8217;\u0430 \u0434\u043b\u044f \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0439 \u0441\u0438\u0442\u0443\u0430\u0446\u0438\u0438. \u041f\u0443\u0441\u0442\u044c \u043c\u044b \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u043c \u0441 \u0431\u0438\u0442\u043e\u0432\u044b\u043c\u0438 \u0432\u0435\u043a\u0442\u043e\u0440\u0430\u043c\u0438 \u0444\u0438\u043a\u0441\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0439 \u0434\u043b\u0438\u043d\u044b. \u041f\u0440\u0438 \u044d\u0442\u043e\u043c, \u0443 \u043d\u0430\u0441 \u0435\u0441\u0442\u044c \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u0443\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u0434\u043b\u0438\u043d\u0443 \u0432\u0435\u043a\u0442\u043e\u0440\u0430 \u043f\u0440\u044f\u043c\u043e \u0432 \u0442\u0438\u043f\u0435. \u041a \u043f\u0440\u0438\u043c\u0435\u0440\u0443, \u0437\u0430\u043f\u0438\u0441\u044c <i>bits: [32]<\/i> \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e <i>bits<\/i> \u2014 \u044d\u0442\u043e 32-\u0431\u0438\u0442\u043d\u044b\u0439 \u0432\u0435\u043a\u0442\u043e\u0440. \u041c\u044b, \u0432 \u043f\u0440\u043e\u0446\u0435\u0441\u0441\u0435 pattern matching&#8217;\u0430, \u0445\u043e\u0442\u0438\u043c \u0438\u043c\u0435\u0442\u044c \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u043c\u0438 \u0441\u043f\u043e\u0441\u043e\u0431\u0430\u043c\u0438 \u0440\u0430\u0437\u0431\u0438\u0432\u0430\u0442\u044c \u0432\u0435\u043a\u0442\u043e\u0440 \u043d\u0430 \u0440\u0430\u0432\u043d\u044b\u0435 \u0447\u0430\u0441\u0442\u0438, \u043a \u043f\u0440\u0438\u043c\u0435\u0440\u0443, \u0442\u0430\u043a:  <\/p>\n<pre><code class=\"haskell\">swapAB : [32] -&gt; [32] swapAB [a b c d] = [b a c d] <\/code><\/pre>\n<p>  \u042d\u0442\u0430 \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 \u043d\u0430 \u0432\u0445\u043e\u0434 32-\u0431\u0438\u0442\u043d\u044b\u0439 \u0432\u0435\u043a\u0442\u043e\u0440, \u0440\u0430\u0437\u0431\u0438\u0432\u0430\u0435\u0442 \u0435\u0433\u043e \u043d\u0430 4 \u0447\u0430\u0441\u0442\u0438, \u043a\u0430\u0436\u0434\u0430\u044f \u0438\u0437 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f 8-\u0431\u0438\u0442\u043d\u044b\u043c \u0432\u0435\u043a\u0442\u043e\u0440\u043e\u043c, \u0438 \u043c\u0435\u043d\u044f\u0435\u0442 \u043f\u0435\u0440\u0432\u044b\u0435 \u0434\u0432\u0430 8-\u0431\u0438\u0442\u043d\u044b\u0445 \u0441\u043b\u043e\u0432\u0430 \u043c\u0435\u0441\u0442\u0430\u043c\u0438. \u041e\u043d\u0430, \u0441 \u0442\u0435\u043c \u0436\u0435 \u0443\u0441\u043f\u0435\u0445\u043e\u043c, \u043c\u043e\u0433\u043b\u0430 \u0440\u0430\u0437\u0431\u0438\u0442\u044c \u0435\u0433\u043e \u0438 \u043d\u0430 2 \u0447\u0430\u0441\u0442\u0438, \u043a\u0430\u0436\u0434\u0430\u044f \u043f\u043e 16-\u0431\u0438\u0442. \u0422\u0430\u043a\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u043f\u043e\u043b\u0435\u0437\u0435\u043d \u043f\u0440\u0438 \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u0438\u0438 \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u041f\u041e. \u041a \u043f\u0440\u0438\u043c\u0435\u0440\u0443, \u043d\u0435\u0447\u0442\u043e \u043f\u043e\u0434\u043e\u0431\u043d\u043e\u0435 \u043b\u0435\u0436\u0438\u0442 \u0432 \u043e\u0441\u043d\u043e\u0432\u0435 \u044f\u0437\u044b\u043a\u0430 Cryptol, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0437\u0430\u0442\u043e\u0447\u0435\u043d \u043f\u043e\u0434 \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u0438\u0435 \u043a\u0440\u0438\u043f\u0442\u043e\u0433\u0440\u0430\u0444\u0438\u0447\u0435\u0441\u043a\u0438\u0445 \u0430\u043b\u0433\u043e\u0440\u0438\u0442\u043c\u043e\u0432. \u041f\u043e\u0441\u043c\u043e\u0442\u0440\u0438\u043c, \u043a\u0430\u043a \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u0442\u044c \u0442\u0430\u043a\u043e\u0435 \u043d\u0430 Agda.<\/p>\n<p>  \u041e\u0431\u0449\u0430\u044f \u0441\u0445\u0435\u043c\u0430 \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u0438 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u043e\u0433\u043e pattern matching&#8217;\u0430 \u0431\u0443\u0434\u0435\u0442 \u0442\u0430\u043a\u0430\u044f:  <\/p>\n<ol>\n<li> \u0420\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u0442\u044c \u0448\u0430\u0431\u043b\u043e\u043d View \u0434\u043b\u044f \u0438\u0441\u0445\u043e\u0434\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430 \u0434\u0430\u043d\u043d\u044b\u0445<br \/> \n<ol>\n<li> \u041e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u0442\u0438\u043f \u0434\u0430\u043d\u043d\u044b\u0445 View, \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u044b \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u044e\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0438\u0441\u0445\u043e\u0434\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430 \u0432 \u043d\u0443\u0436\u043d\u043e\u043c \u043d\u0430\u043c \u0432\u0438\u0434\u0435 <\/li>\n<li> \u041d\u0430\u043f\u0438\u0441\u0430\u0442\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u044e view, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043f\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044e \u0438\u0441\u0445\u043e\u0434\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430 \u0434\u0430\u043d\u043d\u044b\u0445 \u0441\u0442\u0440\u043e\u0438\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 View <\/li>\n<\/ol>\n<\/li>\n<li> \u0418\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c pattern matching \u043d\u0430 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0445 \u0432\u044b\u0437\u043e\u0432\u0430 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 view <\/li>\n<\/ol>\n<p>  \u041f\u0435\u0440\u0435\u0434 \u0442\u0435\u043c \u043a\u0430\u043a \u0440\u0430\u0437\u0431\u0438\u0440\u0430\u0442\u044c\u0441\u044f \u0441 \u044d\u0442\u0438\u043c\u0438 \u043f\u0443\u043d\u043a\u0442\u0430\u043c\u0438, \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u043c \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u0431\u0430\u0437\u043e\u0432\u044b\u0435 \u0442\u0438\u043f\u044b \u0434\u0430\u043d\u043d\u044b\u0445.<\/p>\n<h1>\u041d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u044b\u0435 \u0447\u0438\u0441\u043b\u0430 \u0438 \u0432\u0435\u043a\u0442\u043e\u0440 \u0432 Agda<\/h1>\n<p>  \u041d\u0430\u0442\u0443\u0440\u0430\u043b\u044c\u043d\u044b\u0435 \u0447\u0438\u0441\u043b\u0430 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u044e\u0442\u0441\u044f \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u043e:  <\/p>\n<pre><code class=\"haskell\">data Nat : Set where   Zero : Nat   Suc  : Nat -&gt; Nat <\/code><\/pre>\n<p>  \u041f\u0440\u0438 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0438 \u0442\u0438\u043f\u0430 <i>Nat<\/i>, \u043c\u044b \u0443\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u043c \u0435\u0433\u043e \u0442\u0438\u043f! \u0422\u0430\u043a \u0436\u0435 \u043a\u0430\u043a \u0447\u0438\u0441\u043b\u043e 3 \u0438\u043c\u0435\u0435\u0442 \u0442\u0438\u043f <i>Nat<\/i>, \u0441\u0430\u043c \u043f\u043e \u0441\u0435\u0431\u0435 \u0442\u0438\u043f <i>Nat<\/i> \u0438\u043c\u0435\u0435\u0442 \u0442\u0438\u043f <i>Set<\/i>. <i>Set<\/i> \u2014 \u044d\u0442\u043e \u0432\u0441\u0442\u0440\u043e\u0435\u043d\u043d\u044b\u0439 \u0442\u0438\u043f Agda. \u041e\u0434\u043d\u0430\u043a\u043e, \u043f\u043e\u043d\u0438\u043c\u0430\u043d\u0438\u0435, \u0437\u0430\u0447\u0435\u043c \u044d\u0442\u043e \u043d\u0443\u0436\u043d\u043e, \u043d\u0430\u043c \u043d\u0435 \u043f\u0440\u0438\u0433\u043e\u0434\u0438\u0442\u0441\u044f, \u0438 \u043c\u043e\u0436\u043d\u043e \u043f\u0440\u043e\u0441\u0442\u043e \u0441\u0447\u0438\u0442\u0430\u0442\u044c, \u0447\u0442\u043e \u0432\u0441\u0435 \u0442\u0438\u043f\u044b \u0438\u043c\u0435\u044e\u0442 \u0442\u0438\u043f <i>Set<\/i>, \u0445\u043e\u0442\u044f \u044d\u0442\u043e \u043d\u0435 \u043f\u0440\u0430\u0432\u0434\u0430.<br \/>  \u0423 \u0442\u0438\u043f\u0430 <i>Nat<\/i> \u0434\u0432\u0430 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u0430: <i>Zero<\/i>, \u0443 \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u043d\u0435\u0442 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u043e\u0432, \u0438 <i>Suc<\/i> \u2014 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 \u0441 \u043e\u0434\u043d\u0438\u043c \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u043e\u043c. \u0427\u0438\u0441\u043b\u043e 3, \u0442\u0430\u043a\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c, \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u043a\u0430\u043a <i>(Suc (Suc (Suc Zero)))<\/i>, \u0442\u043e \u0435\u0441\u0442\u044c \u0447\u0442\u043e-\u0442\u043e \u0432\u0440\u043e\u0434\u0435 (1 + (1 + (1 + 0))). \u041e\u0434\u043d\u0430\u043a\u043e, \u0432 Agda \u0435\u0441\u0442\u044c \u0432\u0441\u0442\u0440\u043e\u0435\u043d\u043d\u044b\u0435 \u043b\u0438\u0442\u0435\u0440\u0430\u043b\u044b, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u0432\u043c\u0435\u0441\u0442\u043e \u0434\u043b\u0438\u043d\u043d\u043e\u0439 \u0446\u0435\u043f\u043e\u0447\u043a\u0438 <i>Suc<\/i> \u043c\u043e\u0436\u043d\u043e \u043f\u0440\u043e\u0441\u0442\u043e \u043f\u0438\u0441\u0430\u0442\u044c 3.<\/p>\n<p>  \u0412\u0435\u043a\u0442\u043e\u0440 \u2014 \u044d\u0442\u043e \u0441\u043f\u0438\u0441\u043e\u043a \u0444\u0438\u043a\u0441\u0438\u0440\u043e\u0432\u0430\u043d\u043d\u043e\u0439 \u0434\u043b\u0438\u043d\u044b, \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u044f\u0435\u0442\u0441\u044f \u0442\u0430\u043a:  <\/p>\n<pre><code class=\"haskell\">data Vec (A : Set) : Nat -&gt; Set where   [] : Vec A Zero   _::_ : {n : Nat} -&gt; A -&gt; Vec A n -&gt; Vec A (Suc n) <\/code><\/pre>\n<p>  \u0422\u0438\u043f <i>Vec<\/i>, \u0432 \u043e\u0442\u043b\u0438\u0447\u0438\u0435 \u043e\u0442 <i>Nat<\/i>, \u0438\u043c\u0435\u0435\u0442 2 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0430: \u0442\u0438\u043f <i>A<\/i> \u0438 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 <i>Nat<\/i>. \u0411\u043b\u0430\u0433\u043e\u0434\u0430\u0440\u044f \u0442\u043e\u043c\u0443, \u0447\u0442\u043e \u0432\u0442\u043e\u0440\u043e\u0439 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440 <i>Vec<\/i> \u2014 \u044d\u0442\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435, \u0430 \u043d\u0435 \u0442\u0438\u043f, <i>Vec<\/i> \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c \u0442\u0438\u043f\u043e\u043c. \u0422\u043e\u0442 \u0444\u0430\u043a\u0442, \u0447\u0442\u043e \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u044b \u043e\u0442\u0434\u0435\u043b\u0435\u043d\u044b \u0434\u0440\u0443\u0433 \u043e\u0442 \u0434\u0440\u0443\u0433\u0430 \u0434\u0432\u043e\u0435\u0442\u043e\u0447\u0438\u0435\u043c, \u0430 \u043d\u0435, \u0441\u043a\u0430\u0436\u0435\u043c, \u0441\u0438\u043c\u0432\u043e\u043b\u043e\u043c <i>-&gt;<\/i> \u2014 \u043d\u0435 \u0441\u043e\u0432\u043f\u0430\u0434\u0435\u043d\u0438\u0435. \u041d\u0430 \u0441\u0430\u043c\u043e\u043c \u0434\u0435\u043b\u0435, \u0442\u043e, \u0447\u0442\u043e \u0437\u0430\u043f\u0438\u0441\u0430\u043d\u043e \u043f\u043e\u0441\u043b\u0435 \u0434\u0432\u043e\u0435\u0442\u043e\u0447\u0438\u044f \u2014 \u044d\u0442\u043e \u0442\u0430\u043a \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u043c\u044b\u0435 \u0438\u043d\u0434\u0435\u043a\u0441\u044b, \u0430 \u043d\u0435 \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u044b. \u041e\u0434\u043d\u0430\u043a\u043e, \u0434\u043b\u044f \u043d\u0430\u0441 \u044d\u0442\u043e \u043e\u0442\u043b\u0438\u0447\u0438\u0435 \u043d\u0435 \u0431\u0443\u0434\u0435\u0442 \u0438\u0433\u0440\u0430\u0442\u044c \u043e\u0441\u043e\u0431\u043e\u0433\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0438 \u043c\u044b \u0431\u0443\u0434\u0435\u043c \u0432\u0441\u0451 \u043d\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0430\u043c\u0438.<br \/>  \u041f\u0435\u0440\u0432\u044b\u0439 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 \u0441\u0442\u0440\u043e\u0438\u0442 \u043f\u0443\u0441\u0442\u043e\u0439 \u0432\u0435\u043a\u0442\u043e\u0440. \u0412 Agda \u0432 \u043a\u0430\u0447\u0435\u0441\u0442\u0432\u0435 \u0438\u043c\u0451\u043d \u043c\u043e\u0436\u043d\u043e \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u0440\u0430\u0437\u043d\u044b\u0435 \u043f\u043e\u0441\u043b\u0435\u0434\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u043d\u043e\u0441\u0442\u0438 \u0441\u0438\u043c\u0432\u043e\u043b\u043e\u0432, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u043d\u0430\u0437\u0432\u0430\u0442\u044c \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440<i> []<\/i>.<br \/>  \u0412\u0442\u043e\u0440\u043e\u0439 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442 3 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430 \u2014 \u0440\u0430\u0437\u043c\u0435\u0440 \u0432\u0435\u043a\u0442\u043e\u0440\u0430 <i>n<\/i>, \u044d\u043b\u0435\u043c\u0435\u043d\u0442 \u0432\u0435\u043a\u0442\u043e\u0440\u0430 \u0442\u0438\u043f\u0430 <i>A<\/i>, \u0432\u0435\u043a\u0442\u043e\u0440 \u0440\u0430\u0437\u043c\u0435\u0440\u0430 <i>n<\/i>, \u0438 \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u0432\u0435\u043a\u0442\u043e\u0440 \u0440\u0430\u0437\u043c\u0435\u0440\u0430 <i>(n + 1)<\/i>. \u0417\u0430\u043c\u0435\u0442\u0438\u043c, \u0447\u0442\u043e \u0434\u043b\u044f \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430, \u0440\u0430\u0432\u043d\u043e \u043a\u0430\u043a \u0438 \u0434\u043b\u044f \u043f\u0435\u0440\u0432\u043e\u0433\u043e \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0430 \u0441\u0430\u043c\u043e\u0433\u043e \u0442\u0438\u043f\u0430 <i>Vec<\/i>, \u043c\u044b \u0443\u043a\u0430\u0437\u0430\u043b\u0438 \u043d\u0435 \u043f\u0440\u043e\u0441\u0442\u043e \u0442\u0438\u043f, \u043d\u043e \u0438 \u0438\u043c\u044f \u2014 <i>n: Nat<\/i>. \u042d\u0442\u043e \u043d\u0443\u0436\u043d\u043e, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u043c\u044b \u0441\u0441\u044b\u043b\u043a\u0430\u0435\u043c\u0441\u044f \u043d\u0430 \u044d\u0442\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u043f\u0440\u0438 \u043e\u0431\u044a\u044f\u0432\u043b\u0435\u043d\u0438\u0438 \u0442\u0440\u0435\u0442\u044c\u0435\u0433\u043e \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430 \u0438 \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u043c\u043e\u0433\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u043f\u0435\u0440\u0432\u044b\u0439 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442 \u0432\u0437\u044f\u0442 \u0432 \u0444\u0438\u0433\u0443\u0440\u043d\u044b\u0435 \u0441\u043a\u043e\u0431\u043a\u0438. \u0422\u0430\u043a \u0432 Agda \u043e\u0431\u0437\u043d\u0430\u0447\u0430\u044e\u0442\u0441\u044f \u043d\u0435\u044f\u0432\u043d\u044b\u0435 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u044b. \u0414\u0435\u043b\u043e \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 <i>n<\/i> \u043c\u043e\u0436\u043d\u043e \u043e\u0434\u043d\u043e\u0437\u043d\u0430\u0447\u043d\u043e \u0432\u043e\u0441\u0441\u0442\u0430\u043d\u043e\u0432\u0438\u0442\u044c \u0438\u0437 \u0442\u0440\u0435\u0442\u044c\u0435\u0433\u043e \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u0430. \u0414\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e, \u043a\u043e\u0433\u0434\u0430 \u043c\u044b \u043f\u0435\u0440\u0435\u0434\u0430\u0451\u043c \u0432\u0435\u043a\u0442\u043e\u0440, \u043c\u044b \u0437\u043d\u0430\u0435\u043c \u0435\u0433\u043e \u0440\u0430\u0437\u043c\u0435\u0440, \u043e\u043d \u0443\u043a\u0430\u0437\u0430\u043d \u0432 \u0442\u0438\u043f\u0435. \u041f\u043e\u044d\u0442\u043e\u043c\u0443, \u043d\u0430 \u0441\u0430\u043c\u043e\u043c \u0434\u0435\u043b\u0435, \u043f\u0435\u0440\u0432\u044b\u0439 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442 \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u043d\u0435 \u043f\u0435\u0440\u0435\u0434\u0430\u0432\u0430\u0442\u044c \u2014 Agda \u0441\u0430\u043c\u0430 \u0434\u043e\u0433\u0430\u0434\u0430\u0435\u0442\u0441\u044f, \u043a\u0430\u043a\u043e\u0439 \u043e\u043d \u0434\u043e\u043b\u0436\u0435\u043d \u0431\u044b\u0442\u044c. \u0422\u0430\u043a\u0438\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c, \u0432\u044b\u0437\u043e\u0432 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u0430 <i>_::_<\/i> \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u043b\u0438\u0431\u043e \u043a\u0430\u043a <i>_::_ {n} a someVec<\/i>, \u043b\u0438\u0431\u043e \u043a\u0430\u043a <i>_::_ a someVec<\/i>. \u041d\u043e \u0438 \u044d\u0442\u043e \u0435\u0449\u0451 \u043d\u0435 \u0432\u0441\u0451! \u0421\u0438\u043c\u0432\u043e\u043b\u044b \u043f\u043e\u0434\u0447\u0451\u0440\u043a\u0438\u0432\u0430\u043d\u0438\u044f \u0432 \u0438\u043c\u0435\u043d\u0438 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u0430, \u043d\u0430 \u0441\u0430\u043c\u043e\u043c \u0434\u0435\u043b\u0435, \u0433\u043e\u0432\u0440\u044f\u0442 \u043e \u0442\u043e\u043c, \u0447\u0442\u043e \u043e\u043d \u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0438\u043d\u0444\u0438\u043a\u0441\u043d\u044b\u043c. \u0414\u0432\u0430 \u044f\u0432\u043d\u044b\u0445 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430 \u043c\u043e\u0436\u043d\u043e \u043f\u0438\u0441\u0430\u0442\u044c \u043d\u0435 \u043f\u043e\u0441\u043b\u0435 \u0438\u043c\u0435\u043d\u0438 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u0430, \u0430 \u0432\u043c\u0435\u0441\u0442\u043e \u043f\u043e\u0434\u0447\u0451\u0440\u043a\u0438\u0432\u0430\u043d\u0438\u0439, \u0440\u0430\u0437\u0434\u0435\u043b\u044f\u044f \u0432\u0441\u0451 \u044d\u0442\u043e \u043f\u0440\u043e\u0431\u0435\u043b\u0430\u043c\u0438. \u0412 \u0438\u0442\u043e\u0433\u0435, \u0432\u043e\u0442 \u043f\u0440\u0438\u043c\u0435\u0440 \u0441\u043e\u0437\u0434\u0430\u043d\u0438\u044f \u0432\u0435\u043a\u0442\u043e\u0440\u0430:  <\/p>\n<pre><code class=\"haskell\">v1 : Vec Nat 2 v1 = 1 :: (2 :: []) <\/code><\/pre>\n<p>  \u0417\u0430\u043c\u0435\u0442\u044c\u0442\u0435, \u0447\u0442\u043e \u043c\u044b \u043d\u0435 \u043c\u043e\u0436\u0435\u043c \u043f\u0438\u0441\u0430\u0442\u044c \u0442\u0430\u043a:  <\/p>\n<pre><code class=\"haskell\">v1 : Vec Nat 3 v1 = 1 :: (2 :: []) <\/code><\/pre>\n<p>  \u041a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 <i>[]<\/i> \u0441\u043e\u0437\u0434\u0430\u0451\u0442 \u0432\u0435\u043a\u0442\u043e\u0440 \u0434\u043b\u0438\u043d\u044b 0, \u043f\u0435\u0440\u0432\u044b\u0439 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 <i>::<\/i> \u2014 \u0432\u0435\u043a\u0442\u043e\u0440 \u0434\u043b\u0438\u043d\u044b 1, \u0432\u0442\u043e\u0440\u043e\u0439 <i>::<\/i> \u2014 \u0432\u0435\u043a\u0442\u043e\u0440 \u0434\u043b\u0438\u043d\u044b 2. \u041f\u043e\u043b\u0443\u0447\u0430\u0435\u043c <i>Vec Nat 2<\/i>, \u0430 \u043d\u0430\u0434\u043e 3. \u0421\u0438\u0441\u0442\u0435\u043c\u0430 \u0432\u044b\u0432\u043e\u0434\u0430 \u0442\u0438\u043f\u043e\u0432 \u043d\u0435 \u0434\u0430\u0441\u0442 \u043d\u0430\u043c \u043a\u043e\u043c\u043f\u0438\u043b\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0442\u0430\u043a\u043e\u0439 \u043a\u043e\u0434.<\/p>\n<p>  \u041a\u0440\u043e\u043c\u0435 \u0432\u0441\u0435\u0433\u043e \u043f\u0440\u043e\u0447\u0435\u0433\u043e, \u043d\u0430\u043c \u043f\u043e\u043d\u0430\u0434\u043e\u0431\u044f\u0442\u0441\u044f \u043d\u0435\u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043e\u043f\u0435\u0440\u0430\u0446\u0438\u0438 \u043d\u0430\u0434 \u0432\u0435\u043a\u0442\u043e\u0440\u0430\u043c\u0438:  <\/p>\n<pre><code class=\"haskell\">_++_ : forall {A m n} -&gt; Vec A m -&gt; Vec A n -&gt; Vec A (m + n) take : forall {A m} -&gt; (n : Nat) -&gt; Vec A (n + m) -&gt; Vec A n drop : forall {A m} -&gt; (n : Nat) -&gt; Vec A (n + m) -&gt; Vec A m <\/code><\/pre>\n<p>  \u042d\u0442\u043e \u043a\u043e\u043d\u043a\u0430\u0442\u0435\u043d\u0430\u0446\u0438\u044f \u0432\u0435\u043a\u0442\u043e\u0440\u043e\u0432, \u043e\u043f\u0435\u0440\u0430\u0446\u0438\u044f \u00ab\u0432\u0437\u044f\u0442\u044c \u043f\u0435\u0440\u0432\u044b\u0435 <i>n<\/i> \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u043e\u0432\u00bb \u0438 \u00ab\u0432\u044b\u0431\u0440\u043e\u0441\u0438\u0442\u044c \u043f\u0435\u0440\u0432\u044b\u0435 <i>n<\/i> \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u043e\u0432\u00bb, \u0430\u043d\u0430\u043b\u043e\u0433\u0438\u0447\u043d\u044b\u0435 \u0442\u0435\u043c, \u0447\u0442\u043e \u0435\u0441\u0442\u044c \u0434\u043b\u044f \u0441\u043f\u0438\u0441\u043a\u0430 \u0432 Haskell. \u0417\u0430\u043f\u0438\u0441\u044c \u0432\u0440\u043e\u0434\u0435 <i>forall {A m n}<\/i> \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e, \u043f\u043e\u043c\u0438\u043c\u043e \u0442\u043e\u0433\u043e, \u0447\u0442\u043e \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u044b <i>A<\/i>, <i>m<\/i> \u0438 <i>n<\/i> \u043d\u0435\u044f\u0432\u043d\u044b\u0435, \u0442\u0430\u043a \u043c\u044b \u0435\u0449\u0451 \u0438 \u043d\u0435 \u0445\u043e\u0442\u0438\u043c \u0443\u043a\u0430\u0437\u044b\u0432\u0430\u0442\u044c \u0438\u0445 \u0442\u0438\u043f \u0438 \u043f\u0440\u043e\u0441\u0438\u043c Agda \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0438\u0442\u044c \u0435\u0433\u043e \u043d\u0430 \u043e\u0441\u043d\u043e\u0432\u0435 \u044f\u0432\u043d\u044b\u0445 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u043e\u0432, \u0447\u0442\u043e \u043e\u043f\u044f\u0442\u044c \u0436\u0435 \u043f\u0440\u043e\u0438\u0441\u0445\u043e\u0434\u0438\u0442 \u043e\u0447\u0435\u0432\u0438\u0434\u043d\u044b\u043c \u043e\u0431\u0440\u0430\u0437\u043e\u043c.<\/p>\n<h1>\u0422\u0438\u043f \u0431\u0438\u0442\u043e\u0432\u043e\u0433\u043e \u0432\u0435\u043a\u0442\u043e\u0440\u0430<\/h1>\n<p>  \u0422\u0438\u043f \u0431\u0438\u0442\u043e\u0432\u043e\u0433\u043e \u0432\u0435\u043a\u0442\u043e\u0440\u0430, \u0434\u043b\u044f \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u043c\u044b \u0431\u0443\u0434\u0435\u043c \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u044b\u0432\u0430\u0442\u044c pattern matching, \u0431\u0443\u0434\u0435\u0442 \u0432\u044b\u0433\u043b\u044f\u0434\u0435\u0442\u044c \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u043f\u0440\u043e\u0441\u0442\u043e:  <\/p>\n<pre><code class=\"haskell\">data Bit : Set where   O : Bit   I : Bit  Word : Nat -&gt; Set Word n = Vec Bit n <\/code><\/pre>\n<p>  <i>Word<\/i> \u2014 \u044d\u0442\u043e \u0441\u0438\u043d\u043e\u043d\u0438\u043c \u0434\u043b\u044f <i>Vec Bit<\/i>, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044f \u0435\u0433\u043e \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u043e\u0431\u044a\u044f\u0432\u043b\u044f\u0442\u044c 32-\u0431\u0438\u0442\u043d\u044b\u0439 \u0432\u0435\u043a\u0442\u043e\u0440 \u043a\u0430\u043a <i>bits: Word 32<\/i>.<br \/>  \u041f\u0435\u0440\u0435\u0434 \u0442\u0435\u043c, \u043a\u0430\u043a \u043f\u0435\u0440\u0435\u0439\u0442\u0438 \u043a pattern matching&#8217;\u0443, \u043f\u043e\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u043d\u0430 \u0435\u0433\u043e \u043e\u0441\u043e\u0431\u0435\u043d\u043d\u043e\u0441\u0442\u0438 \u0432 \u043f\u0440\u0438\u0441\u0443\u0442\u0441\u0442\u0432\u0438\u0438 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432.<\/p>\n<h1>\u041e\u0441\u043e\u0431\u0435\u043d\u043d\u043e\u0441\u0442\u0438 pattern matching \u0432 \u043f\u0440\u0438\u0441\u0443\u0442\u0441\u0442\u0432\u0438\u0438 \u0437\u0430\u0432\u0438c\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432<\/h1>\n<p>  \u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0438\u0439 \u0442\u0438\u043f \u0434\u0430\u043d\u043d\u044b\u0445:  <\/p>\n<pre><code class=\"haskell\">data _==_ {A : Set} : A -&gt; A -&gt; Set where   Refl : {x : A} -&gt; x == x <\/code><\/pre>\n<p>  \u0422\u0438\u043f <i>(x == y)<\/i> \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0438\u0437\u0443\u0435\u0442\u0441\u044f \u0434\u0432\u0443\u043c\u044f \u043a\u043e\u043d\u043a\u0440\u0435\u0442\u043d\u044b\u043c\u0438 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f\u043c\u0438 \u0442\u0438\u043f\u0430 <i>A<\/i> \u0438, \u043a\u0430\u043a \u043d\u0435\u0441\u043b\u043e\u0436\u043d\u043e \u0434\u043e\u0433\u0430\u0434\u0430\u0442\u044c\u0441\u044f, \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442 \u0443\u0442\u0432\u0435\u0440\u0436\u0434\u0435\u043d\u0438\u0435 \u043e \u0442\u043e\u043c, \u0447\u0442\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f <i>x<\/i> \u0438 <i>y<\/i> \u0440\u0430\u0432\u043d\u044b. \u041d\u0430\u043b\u0438\u0447\u0438\u0435 \u0435\u0434\u0438\u043d\u0441\u0442\u0432\u0435\u043d\u043d\u043e\u0433\u043e \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u0430 <i>Refl<\/i> \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u0435\u0442, \u0447\u0442\u043e \u043c\u044b \u043d\u0435 \u043c\u043e\u0436\u0435\u043c \u0441\u043e\u0437\u0434\u0430\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0442\u0438\u043f\u0430 <i>(x == y)<\/i> \u0434\u043b\u044f \u0440\u0430\u0437\u043d\u044b\u0445 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0439 <i>x<\/i> \u0438 <i>y<\/i>. \u041a \u043f\u0440\u0438\u043c\u0435\u0440\u0443:  <\/p>\n<pre><code class=\"haskell\">eq : (3 == 3) eq = Refl  notEq : (3 == 4) notEq = ? <\/code><\/pre>\n<p>  \u0412 \u043f\u0435\u0440\u0432\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435 \u043d\u0430\u043c \u043d\u0443\u0436\u043d\u043e \u0441\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 <i>(3 == 3)<\/i> \u0438 \u0443 \u043d\u0430\u0441 \u0435\u0441\u0442\u044c \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u044d\u0442\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c \u2014 <i>Refl<\/i>. \u0417\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0436\u0435 \u0442\u0438\u043f\u0430 <i>(3 == 4)<\/i> \u043c\u044b \u0441\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u043d\u0435 \u043c\u043e\u0436\u0435\u043c \u2014 <i>Refl<\/i> \u043d\u0435 \u043f\u043e\u0434\u0445\u043e\u0434\u0438\u0442 \u043f\u043e \u0442\u0438\u043f\u0443, \u0430 \u0434\u0440\u0443\u0433\u0438\u0445 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u043e\u0432 \u0443 \u0442\u0438\u043f\u0430 <i>==<\/i> \u043d\u0435\u0442.<br \/>  \u0422\u0435\u043f\u0435\u0440\u044c \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0442\u0430\u043a\u0443\u044e \u0444\u0443\u043d\u043a\u0446\u0438\u044e:  <\/p>\n<pre><code class=\"haskell\">f : (x : Nat) -&gt; (y : Nat) -&gt; (x == y) -&gt; Nat <\/code><\/pre>\n<p>  \u041a\u0430\u043a \u0431\u0443\u0434\u0435\u0442 \u0432\u044b\u0433\u043b\u044f\u0434\u0435\u0442\u044c pattern matching \u0434\u043b\u044f \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u043e\u0432 \u044d\u0442\u043e\u0439 \u0444\u0443\u043d\u043a\u0446\u0438\u0438? \u041e\u0447\u0435\u0432\u0438\u0434\u043d\u043e, \u0447\u0442\u043e \u0434\u043b\u044f \u0442\u0440\u0435\u0442\u044c\u0435\u0433\u043e \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430 \u043c\u044b \u043d\u0430\u043f\u0438\u0448\u0435\u043c <i>Refl<\/i>, \u0442\u0430\u043a \u043a\u0430\u043a \u0434\u0440\u0443\u0433\u0438\u0445 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440\u043e\u0432 \u0443 \u0442\u0438\u043f\u0430 <i>==<\/i> \u043d\u0435\u0442. \u041f\u0440\u0438 \u044d\u0442\u043e\u043c, \u043c\u044b \u0430\u0432\u0442\u043e\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0443\u0437\u043d\u0430\u0451\u043c, \u0447\u0442\u043e \u043f\u0435\u0440\u0432\u044b\u0439 \u0438 \u0432\u0442\u043e\u0440\u043e\u0439 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442 \u2014 \u044d\u0442\u043e \u043e\u0434\u043d\u043e \u0438 \u0442\u043e \u0436\u0435 \u0447\u0438\u0441\u043b\u043e! \u0412 \u043f\u043e\u0434\u043e\u0431\u043d\u044b\u0445 \u0441\u043b\u0443\u0447\u0430\u044f\u0445, \u0432 Agda \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u044f\u0432\u043d\u043e \u043e\u0442\u043c\u0435\u0442\u0438\u0442\u044c \u044d\u0442\u043e\u0442 \u0444\u0430\u043a\u0442 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044f \u0442\u0430\u043a \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u043c\u044b\u0439 dot pattern:  <\/p>\n<pre><code class=\"haskell\">f x .x Refl = x <\/code><\/pre>\n<p>  \u0422\u0430\u043a\u0430\u044f \u0437\u0430\u043f\u0438\u0441\u044c \u043e\u0437\u043d\u0430\u0447\u0430\u0435\u0442, \u0447\u0442\u043e \u0432\u0442\u043e\u0440\u043e\u0439 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442 (\u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0438\u043c\u0435\u0435\u0442 \u0442\u0430\u043a\u043e\u0435 \u0436\u0435 \u0438\u043c\u044f \u043a\u0430\u043a \u043f\u0435\u0440\u0432\u044b\u0439 \u0441 \u043f\u0440\u0438\u043f\u0438\u0441\u0430\u043d\u043d\u043e\u0439 \u0442\u043e\u0447\u043a\u043e\u0439) \u2014 \u044d\u0442\u043e \u0442\u043e \u0436\u0435 \u0441\u0430\u043c\u043e\u0435, \u0447\u0442\u043e \u0441\u043e\u043f\u043e\u0441\u0442\u0430\u0432\u0438\u043b\u043e\u0441\u044c \u0441 \u043f\u0435\u0440\u0432\u044b\u043c \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u043e\u043c. \u041c\u044b \u043d\u0435 \u043c\u043e\u0436\u0435\u043c \u043d\u0430\u043f\u0438\u0441\u0430\u0442\u044c, \u0441\u043a\u0430\u0436\u0435\u043c, <i>y<\/i> \u0432\u043c\u0435\u0441\u0442\u043e <i>.x<\/i>, \u0442\u0430\u043a \u043a\u0430\u043a \u043d\u0435 \u0445\u043e\u0442\u0438\u043c \u0442\u0435\u0440\u044f\u0442\u044c \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e \u043e \u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0435, \u043a\u043e\u0442\u043e\u0440\u0443\u044e \u043f\u043e\u043b\u0443\u0447\u0438\u043b\u0438 \u043f\u043e\u0441\u043b\u0435 \u0441\u043e\u043f\u043e\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u044f \u0441 <i>Refl<\/i>.<\/p>\n<p>  \u0412\u044b\u0432\u043e\u0434 \u043e\u0442\u0441\u044e\u0434\u0430 \u0442\u0430\u043a\u043e\u0439: \u0432 \u044f\u0437\u044b\u043a\u0430\u0445 \u0441 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438, \u043f\u043e\u0441\u043b\u0435 pattern matching&#8217;\u0430 \u043d\u0430 \u043a\u0430\u043a\u043e\u043c-\u043b\u0438\u0431\u043e \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0435, \u043c\u044b \u043c\u043e\u0436\u0435\u043c \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u0434\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u0443\u044e \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e \u043e \u0434\u0440\u0443\u0433\u0438\u0445 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430\u0445.<\/p>\n<h1>Views<\/h1>\n<p>  \u041f\u0435\u0440\u0435\u0434 \u0442\u0435\u043c \u043a\u0430\u043a \u043f\u043e\u0441\u0442\u0440\u043e\u0438\u0442\u044c View \u0434\u043b\u044f \u043d\u0430\u0448\u0435\u0433\u043e \u0442\u0438\u043f\u0430 <i>Word<\/i>, \u0440\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0431\u043e\u043b\u0435\u0435 \u043f\u0440\u043e\u0441\u0442\u043e\u0439 \u043f\u0440\u0438\u043c\u0435\u0440, \u0447\u0442\u043e\u0431\u044b \u043f\u043e\u043d\u044f\u0442\u044c, \u0447\u0435\u0433\u043e \u043c\u044b \u0445\u043e\u0442\u0438\u043c \u0434\u043e\u0441\u0442\u0438\u0447\u044c.<br \/>  \u0420\u0430\u0441\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0442\u0438\u043f \u0441\u043f\u0438\u0441\u043a\u0430:  <\/p>\n<pre><code class=\"haskell\">data List (A : Set) : Set where   [] : List A   _::_ : A -&gt; List A -&gt; List A <\/code><\/pre>\n<p>  \u042d\u0442\u043e \u043e\u0431\u044b\u0447\u043d\u044b\u0439 \u0441\u043f\u0438\u0441\u043e\u043a, \u0442\u0430\u043a\u043e\u0439 \u0436\u0435, \u043a\u0430\u043a \u0432 Haskell, \u043e\u043d \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u043e, \u043a\u0430\u043a \u00ab\u043f\u0435\u0440\u0432\u044b\u0439 \u044d\u043b\u0435\u043c\u0435\u043d\u0442 \u0438 \u0441\u043f\u0438\u0441\u043e\u043a\u00bb. \u041c\u044b \u0445\u043e\u0442\u0438\u043c \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c \u0432\u043e\u0437\u043c\u043e\u0436\u043d\u043e\u0441\u0442\u044c \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u0438\u0442\u044c \u0442\u043e\u0442 \u0436\u0435 \u0441\u0430\u043c\u044b\u0439 \u0441\u043f\u0438\u0441\u043e\u043a \u043a\u0430\u043a \u00ab\u0441\u043f\u0438\u0441\u043e\u043a \u0438 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0439 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u00bb. \u0417\u0430\u0432\u0435\u0434\u0451\u043c \u0434\u043b\u044f \u044d\u0442\u043e\u0433\u043e \u0442\u0438\u043f \u0434\u0430\u043d\u043d\u044b\u0445 <i>SnocView<\/i>:  <\/p>\n<pre><code class=\"haskell\">data SnocView {A : Set} : List A -&gt; Set where   [] : SnocView []   _:::_ : (xs : List A) -&gt; (x : A) -&gt; SnocView (xs ++ (x :: [])) <\/code><\/pre>\n<p>  \u0417\u0434\u0435\u0441\u044c \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u043e\u043f\u0435\u0440\u0430\u0442\u043e\u0440 <i>++<\/i> \u2014 \u044d\u0442\u043e \u043a\u043e\u043d\u043a\u0430\u0442\u0435\u043d\u0430\u0446\u0438\u044f \u0441\u043f\u0438\u0441\u043a\u043e\u0432, \u043a\u0430\u043a \u0432 Haskell. \u041f\u0440\u0438\u043c\u0435\u0440 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0442\u0438\u043f\u0430 <i>SnocView<\/i>:  <\/p>\n<pre><code class=\"haskell\">sx : SnocView (1 :: 2 :: 3 :: []) sx = (1 :: 2 :: []) ::: 3 <\/code><\/pre>\n<p>  \u0417\u0430\u043c\u0435\u0442\u044c\u0442\u0435, \u0447\u0442\u043e \u0442\u0438\u043f <i>SnocView<\/i> \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0438\u0437\u0443\u0435\u0442\u0441\u044f \u0441\u043f\u0438\u0441\u043a\u043e\u043c, \u0434\u043b\u044f \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u0441\u0442\u0440\u043e\u0438\u0442\u0441\u044f \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u043b\u0435\u043d\u0438\u0435 \u00ab\u0441\u043f\u0438\u0441\u043e\u043a \u0438 \u043f\u043e\u0441\u043b\u0435\u0434\u043d\u0438\u0439 \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u00bb.<br \/>  \u0422\u0435\u043f\u0435\u0440\u044c \u043d\u0430\u043f\u0438\u0448\u0435\u043c \u0444\u0443\u043d\u043a\u0446\u0438\u044e <i>snocView<\/i>, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0434\u043b\u044f \u043f\u0435\u0440\u0435\u0434\u0430\u043d\u043d\u043e\u0433\u043e \u0441\u043f\u0438\u0441\u043a\u0430 \u0441\u0442\u0440\u043e\u0438\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 <i>SnocView<\/i>:  <\/p>\n<pre><code class=\"haskell\">snocView : {A : Set} -&gt; (xs : List A) -&gt; SnocView xs snocView [] = [] snocView (x :: xs)              with snocView xs snocView (x :: .[])                | []       = [] ::: x snocView (x :: .(ys ++ (y :: []))) | ys ::: y = (x :: ys) ::: y <\/code><\/pre>\n<p>  \u0417\u0434\u0435\u0441\u044c \u043c\u043d\u043e\u0433\u043e \u0432\u0441\u0435\u0433\u043e, \u043d\u0430\u0447\u043d\u0451\u043c \u043f\u043e \u043f\u043e\u0440\u044f\u0434\u043a\u0443. \u0421\u043b\u0443\u0447\u0430\u0439 \u0441 \u043f\u0443\u0441\u0442\u044b\u043c \u0441\u043f\u0438\u0441\u043a\u043e\u043c \u043e\u0447\u0435\u0432\u0438\u0434\u0435\u043d: \u043f\u0443\u0441\u0442\u043e\u0439 \u0441\u043f\u0438\u0441\u043e\u043a \u0434\u0430\u0451\u0442 \u0442\u0440\u0438\u0432\u0438\u0430\u043b\u044c\u043d\u044b\u0439 <i>SnocView<\/i>. \u0414\u0430\u043b\u0435\u0435, \u0435\u0441\u043b\u0438 \u0441\u043f\u0438\u0441\u043e\u043a \u043d\u0435 \u043f\u0443\u0441\u0442, \u043c\u044b \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u043c \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044e with (\u0434\u043b\u0438\u043d\u043d\u044b\u0435 \u043e\u0442\u0441\u0442\u0443\u043f\u044b \u0437\u0434\u0435\u0441\u044c \u0442\u043e\u043b\u044c\u043a\u043e \u0434\u043b\u044f \u0443\u0434\u043e\u0431\u0441\u0442\u0432\u0430 \u0447\u0442\u0435\u043d\u0438\u044f). \u042d\u0442\u043e \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044f \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u0442 \u043f\u0440\u0438\u043c\u0435\u0440\u043d\u043e \u0442\u0435 \u0436\u0435 \u0437\u0430\u0434\u0430\u0447\u0438, \u0447\u0442\u043e \u0438 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044f case of \u0432 Haskell, \u0442\u043e \u0435\u0441\u0442\u044c \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u0435\u0442\u0441\u044f \u0434\u043b\u044f \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u044f pattern matching \u0432 \u0442\u0435\u043b\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438. \u041e\u0431\u0440\u0430\u0437\u0446\u044b, \u0441 \u043a\u043e\u0442\u043e\u0440\u044b\u043c\u0438 \u043c\u044b \u0441\u043e\u043f\u043e\u0441\u0442\u0430\u0432\u043b\u044f\u0435\u043c \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u044b\u0439 \u0432\u044b\u0437\u043e\u0432 <i>snocView xs<\/i>, \u0443\u043a\u0430\u0437\u0430\u043d\u044b \u0441\u043f\u0440\u0430\u0432\u0430 \u043e\u0442 \u0432\u0435\u0440\u0442\u0438\u043a\u0430\u043b\u044c\u043d\u044b\u0445 \u0447\u0451\u0440\u0442\u043e\u0447\u0435\u043a. \u0418\u0442\u0430\u043a, \u0435\u0441\u043b\u0438 \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u044b\u0439 \u0432\u044b\u0437\u043e\u0432 \u0434\u0430\u043b \u043d\u0430\u043c \u0442\u0440\u0438\u0432\u0438\u0430\u043b\u044c\u043d\u044b\u0439 <i>SnocView<\/i>, \u0437\u043d\u0430\u0447\u0438\u0442 \u0441\u043f\u0438\u0441\u043e\u043a <i>xs<\/i> \u0431\u044b\u043b \u043f\u0443\u0441\u0442, \u043f\u043e\u044d\u0442\u043e\u043c\u0443 <i>SnocView<\/i> \u0434\u043b\u044f <i>x :: []<\/i> \u2014 \u044d\u0442\u043e <i>[] ::: x<\/i>. \u0412\u043e \u0432\u0442\u043e\u0440\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435, \u043c\u044b \u043f\u043e\u043b\u0443\u0447\u0430\u0435\u043c, \u0447\u0442\u043e <i>SnocView<\/i> \u0434\u043b\u044f <i>xs<\/i> \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u043a\u0430\u043a <i>ys ::: y<\/i>, \u043f\u043e\u044d\u0442\u043e\u043c\u0443, \u0447\u0442\u043e\u0431\u044b \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u044c <i>SnocView<\/i> \u0434\u043b\u044f <i>x :: xs<\/i> \u043d\u0443\u0436\u043d\u043e \u0434\u043e\u0431\u0430\u0432\u0438\u0442\u044c <i>x<\/i> \u0432 \u0433\u043e\u043b\u043e\u0432\u0443 <i>ys<\/i>.<br \/>  \u041d\u0435\u043f\u043e\u043d\u044f\u0442\u043d\u044b\u043c \u043e\u0441\u0442\u0430\u043b\u043e\u0441\u044c \u043b\u0438\u0448\u044c \u0442\u043e, \u0447\u0442\u043e \u0443\u043a\u0430\u0437\u0430\u043d\u043e \u0441\u043b\u0435\u0432\u0430 \u043e\u0442 \u0432\u0435\u0440\u0442\u0438\u043a\u0430\u043b\u044c\u043d\u044b\u0445 \u0447\u0451\u0440\u0442\u043e\u0447\u0435\u043a. \u041a\u0430\u043a \u043c\u044b \u043e\u0431\u0441\u0443\u0436\u0434\u0430\u043b\u0438 \u0440\u0430\u043d\u0435\u0435, pattern matching \u0432 \u043f\u0440\u0438\u0441\u0443\u0442\u0441\u0442\u0432\u0438\u0438 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432 \u043c\u043e\u0436\u0435\u0442 \u0434\u0430\u0432\u0430\u0442\u044c \u043d\u0430\u043c \u0434\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u0443\u044e \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e \u043e \u0434\u0440\u0443\u0433\u0438\u0445 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u0430\u0445 \u0444\u0443\u043d\u043a\u0446\u0438\u0438. \u0412 \u043d\u0430\u0448\u0435\u043c \u043f\u0440\u0438\u043c\u0435\u0440\u0435, pattern matching \u043d\u0430 \u0440\u0435\u043a\u0443\u0440\u0441\u0438\u0432\u043d\u043e\u043c \u0432\u044b\u0437\u043e\u0432\u0435 <i>snocView xs<\/i> \u0434\u0430\u0451\u0442 \u043d\u0430\u043c \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e \u043e \u0442\u043e\u043c, \u043a\u0430\u043a\u043e\u0435 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0438\u043c\u0435\u0435\u0442 \u0441\u043f\u0438\u0441\u043e\u043a <i>xs<\/i>. \u0418\u043c\u0435\u043d\u043d\u043e \u044d\u0442\u0430 \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044f \u0438 \u0443\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e dot patterns \u0441\u043b\u0435\u0432\u0430 \u043e\u0442 \u0432\u0435\u0440\u0442\u0438\u043a\u0430\u043b\u044c\u043d\u043e\u0439 \u0447\u0435\u0440\u0442\u044b. \u041a \u043f\u0440\u0438\u043c\u0435\u0440\u0443, \u0432\u043e \u0432\u0442\u043e\u0440\u043e\u043c \u0441\u043b\u0443\u0447\u0430\u0435, \u0443\u0437\u043d\u0430\u0432, \u0447\u0442\u043e <i>snocView xs<\/i> \u0434\u0430\u0451\u0442 \u043d\u0430\u043c <i>ys ::: y<\/i>, \u043c\u044b \u043f\u043e\u043d\u0438\u043c\u0430\u0435\u043c, \u0447\u0442\u043e \u0441\u043f\u0438\u0441\u043e\u043a <i>xs<\/i> \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u0443\u0435\u0442\u0441\u044f \u043a\u0430\u043a \u043a\u043e\u043d\u043a\u0430\u0442\u0435\u043d\u0430\u0446\u0438\u044f <i>ys<\/i> \u0438 \u0441\u043f\u0438\u0441\u043a\u0430 \u0438\u0437 \u043e\u0434\u043d\u043e\u0433\u043e \u044d\u043b\u0435\u043c\u0435\u043d\u0442\u0430 <i>y :: []<\/i>.<\/p>\n<p>  \u0412\u043e\u0442 \u043f\u0440\u0438\u043c\u0435\u0440 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044f <i>snocView<\/i> \u0434\u043b\u044f \u043d\u0430\u043f\u0438\u0441\u0430\u043d\u0438\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0446\u0438\u043a\u043b\u0438\u0447\u0435\u0441\u043a\u0438 \u0441\u0434\u0432\u0438\u0433\u0430\u0435\u0442 \u043f\u0435\u0440\u0435\u0434\u0430\u043d\u043d\u044b\u0439 \u0441\u043f\u0438\u0441\u043e\u043a \u0432\u043f\u0440\u0430\u0432\u043e:  <\/p>\n<pre><code class=\"haskell\">rotateRight : {A : Set} -&gt; List A -&gt; List A rotateRight xs with snocView xs rotateRight ._ | [] = [] rotateRight ._ | ys ::: y = y :: ys <\/code><\/pre>\n<p>  \u0417\u0434\u0435\u0441\u044c \u043c\u044b \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043b\u0438 \u0441\u0438\u043c\u0432\u043e\u043b\u044b \u043f\u043e\u0434\u0447\u0451\u0440\u043a\u0438\u0432\u0430\u043d\u0438\u044f. \u0422\u0430\u043a \u043c\u043e\u0436\u043d\u043e \u0434\u0435\u043b\u0430\u0442\u044c, \u043a\u043e\u0433\u0434\u0430 \u043d\u0430\u0441 \u043d\u0435 \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u0443\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435, \u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u0434\u043e\u043b\u0436\u043d\u043e \u0431\u044b\u0442\u044c \u043d\u0430 \u043c\u0435\u0441\u0442\u0435 \u043f\u043e\u0434\u0447\u0451\u0440\u043a\u0438\u0432\u0430\u043d\u0438\u0439. \u0412\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u0434\u043e\u0432\u043e\u043b\u044c\u043d\u043e \u043a\u0440\u0430\u0442\u043a\u043e \u0438 \u043a\u0440\u0430\u0441\u0438\u0432\u043e! \u042d\u0442\u043e\u0442 \u043f\u0440\u0438\u043c\u0435\u0440, \u043f\u043e \u0441\u0443\u0442\u0438, \u0438 \u043f\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442, \u043a\u0430\u043a \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u044b\u0432\u0442\u044c \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u0438\u0439 pattern matching \u0432 \u044f\u0437\u044b\u043a\u0430\u0445 \u0441 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438. \u041f\u043e\u0441\u043c\u043e\u0442\u0440\u0438\u043c \u0442\u0435\u043f\u0435\u0440\u044c, \u043a\u0430\u043a \u043f\u0440\u043e\u0432\u0435\u0440\u043d\u0443\u0442\u044c \u0442\u043e\u0436\u0435 \u0441\u0430\u043c\u043e\u0435 \u0434\u043b\u044f \u0442\u0438\u043f\u0430 Word!<\/p>\n<h1>SplitView \u0434\u043b\u044f Word<\/h1>\n<p>  \u041a\u0430\u043a \u0438 \u0432 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u043c \u043f\u0440\u0438\u043c\u0435\u0440\u0435, \u043d\u0430\u043c \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u044b 2 \u0432\u0435\u0449\u0438: \u0441\u043f\u0435\u0446\u0438\u0430\u043b\u044c\u043d\u044b\u0439 \u0442\u0438\u043f \u0434\u0430\u043d\u043d\u044b\u0445 <i>SplitView<\/i> \u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u044f <i>splitView<\/i>, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0431\u0443\u0434\u0435\u0442 \u0441\u0442\u0440\u043e\u0438\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 <i>SplitView<\/i> \u0434\u043b\u044f \u0437\u0430\u0434\u0430\u043d\u043d\u043e\u0433\u043e \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0442\u0438\u043f\u0430 <i>Word<\/i>.<br \/>  \u0414\u043b\u044f \u043d\u0430\u0447\u0430\u043b\u0430, \u043d\u0430\u043c \u043f\u043e\u043d\u0430\u0434\u043e\u0431\u044f\u0442\u0441\u044f 2 \u0434\u043e\u043f\u043e\u043b\u043d\u0438\u0442\u0435\u043b\u044c\u043d\u044b\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0434\u043b\u044f \u0440\u0430\u0431\u043e\u0442\u044b \u0441 \u0442\u0438\u043f\u043e\u043c <i>Vec<\/i>:  <\/p>\n<pre><code class=\"haskell\">split : forall {A} -&gt; (n : Nat) -&gt; (m : Nat) -&gt; Vec A (m * n) -&gt; Vec (Vec A n) m split n Zero [] = [] split n (Suc k) xs = (take n xs) :: (split n k (drop n xs))  concat : forall {A n m } -&gt; Vec (Vec A n) m -&gt; Vec A (m * n) concat [] = [] concat (xs :: xss) = xs ++ concat xss <\/code><\/pre>\n<p>  \u0422\u0438\u043f <i>SplitView<\/i> \u0431\u0443\u0434\u0435\u0442 \u0432\u044b\u0433\u043b\u044f\u0434\u0435\u0442\u044c \u0442\u0430\u043a:  <\/p>\n<pre><code class=\"haskell\">data SplitView {A : Set} : {n : Nat} -&gt; (m : Nat) -&gt; Vec A (m * n) -&gt; Set where   [_] : forall {m n} -&gt; (xss : Vec (Vec A n) m) -&gt; SplitView m (concat xss) <\/code><\/pre>\n<p>  \u042d\u0442\u043e\u0442 \u0442\u0438\u043f \u043f\u0430\u0440\u0430\u043c\u0435\u0442\u0440\u0438\u0437\u0443\u0435\u0442\u0441\u044f \u0447\u0438\u0441\u043b\u043e\u043c <i>m<\/i> \u0438 \u0432\u0435\u043a\u0442\u043e\u0440\u043e\u043c. <i>m<\/i> \u043f\u043e\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442, \u043d\u0430 \u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0447\u0430\u0441\u0442\u0435\u0439 \u043c\u044b \u0445\u043e\u0442\u0438\u043c \u0440\u0430\u0437\u0431\u0438\u0442\u044c \u0432\u0435\u043a\u0442\u043e\u0440. \u0418\u043c\u0435\u043d\u043d\u043e \u043f\u043e\u044d\u0442\u043e\u043c\u0443 \u0434\u043b\u0438\u043d\u0430 \u0432\u0435\u043a\u0442\u043e\u0440\u0430 \u043a\u0440\u0430\u0442\u043d\u0430 <i>m<\/i>. \u0415\u0434\u0438\u043d\u0441\u0442\u0432\u0435\u043d\u043d\u044b\u0439 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 \u043f\u043e\u0437\u0432\u043e\u043b\u0438\u0442 \u043d\u0430\u043c \u0437\u0430\u043f\u0438\u0441\u044b\u0432\u0430\u0442\u044c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0434\u0430\u043d\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430 \u0442\u0430\u043a:  <\/p>\n<pre><code class=\"haskell\">[ a :: b :: c :: d :: [] ] <\/code><\/pre>\n<p>  \u0433\u0434\u0435 a, b, c \u0438 d \u2014 \u0432\u0435\u043a\u0442\u043e\u0440\u044b \u0434\u043b\u0438\u043d\u044b n.<br \/>  \u041d\u0430 \u043e\u0447\u0435\u0440\u0435\u0434\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u044f <i>splitView<\/i>:  <\/p>\n<pre><code class=\"haskell\">splitView : {A : Set} -&gt; (n : Nat) -&gt; (m : Nat) -&gt; (xs : Vec A (m * n)) -&gt; SplitView m xs <\/code><\/pre>\n<p>  \u0427\u0442\u043e\u0431\u044b \u0435\u0451 \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u0430\u0442\u044c, \u043d\u0443\u0436\u043d\u043e \u0440\u0430\u0437\u0431\u0438\u0442\u044c \u043f\u0435\u0440\u0435\u0434\u0430\u043d\u043d\u044b\u0439 \u0432\u0435\u043a\u0442\u043e\u0440 \u043d\u0430 <i>m<\/i> \u0447\u0430\u0441\u0442\u0435\u0439, \u043a\u0430\u0436\u0434\u0430\u044f \u0434\u043b\u0438\u043d\u044b <i>n<\/i>, \u0438 \u043f\u0435\u0440\u0435\u0434\u0430\u0442\u044c \u0432 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 <i>[_]<\/i>:  <\/p>\n<pre><code class=\"haskell\">splitView n m xs = [ split n m xs ] <\/code><\/pre>\n<p>  \u041e\u0434\u043d\u0430\u043a\u043e, \u0442\u0430\u043a\u043e\u0435 \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435 \u043d\u0435 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442\u0441\u044f \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440\u043e\u043c. \u0414\u0435\u043b\u043e \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0442\u043e\u0440 <i>[_]<\/i> \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0442\u0438\u043f\u0430 <i>SplitView m (concat xss)<\/i>. \u0412 \u043d\u0430\u0448\u0435\u043c \u0441\u043b\u0443\u0447\u0430\u0435, <i>xss<\/i> \u2014 \u044d\u0442\u043e <i>split n m xs<\/i>, \u0442\u0430\u043a \u0447\u0442\u043e \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u0435 <i>[ split n m xs ]<\/i> \u0438\u043c\u0435\u0435\u0442 \u0442\u0438\u043f <i>SplitView m (concat (split n m xs))<\/i>. \u041f\u0440\u0438 \u044d\u0442\u043e\u043c, \u0432 \u0441\u0438\u0433\u043d\u0430\u0442\u0443\u0440\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0443\u043a\u0430\u0437\u0430\u043d\u043e, \u0447\u0442\u043e \u043e\u043d\u0430 \u0434\u043e\u043b\u0436\u043d\u0430 \u0432\u0435\u0440\u043d\u0443\u0442\u044c \u0442\u0438\u043f <i>SplitView m xs<\/i>, \u0433\u0434\u0435 <i>xs<\/i> \u2014 \u0442\u0440\u0435\u0442\u0438\u0439 \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442 \u0444\u0443\u043d\u043a\u0446\u0438\u0438. \u041c\u044b \u0441 \u0432\u0430\u043c\u0438 \u043f\u043e\u043d\u0438\u043c\u0430\u0435\u043c, \u0447\u0442\u043e \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f <i>xs<\/i> \u0438 <i>concat (split n m xs)<\/i> \u2014 \u044d\u0442\u043e \u043e\u0434\u043d\u043e \u0438 \u0442\u043e \u0436\u0435, \u043f\u043e\u0442\u043e\u043c\u0443 \u0447\u0442\u043e \u0437\u043d\u0430\u0435\u043c, \u043a\u0430\u043a \u0443\u0441\u0442\u0440\u043e\u0435\u043d\u044b \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <i>concat<\/i> \u0438 <i>split<\/i>. \u0414\u0430\u0432\u0430\u0439\u0442\u0435 \u0443\u0431\u0435\u0434\u0438\u043c \u0432 \u044d\u0442\u043e\u043c \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440.<br \/>  \u0414\u043b\u044f \u043d\u0430\u0447\u0430\u043b\u0430, \u043f\u0435\u0440\u0435\u043f\u0438\u0448\u0435\u043c \u043f\u0440\u0438\u0432\u0435\u0434\u0451\u043d\u043d\u043e\u0435 \u0432\u044b\u0448\u0435 \u0442\u0435\u043b\u043e <i>splitView<\/i> \u0432 \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0435\u0439 \u0444\u043e\u0440\u043c\u0435:  <\/p>\n<pre><code class=\"haskell\">splitView n m xs with [ split n m xs ] splitView n m xs | v = v <\/code><\/pre>\n<p>  \u042d\u0442\u043e \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435 \u043d\u0435 \u043f\u0440\u0438\u043d\u0438\u043c\u0430\u0435\u0442\u0441\u044f \u043a\u043e\u043c\u043f\u0438\u043b\u044f\u0442\u043e\u0440\u043e\u043c \u043f\u043e \u0442\u0435\u043c \u0436\u0435 \u043f\u0440\u0438\u0447\u0438\u043d\u0430\u043c, \u0447\u0442\u043e \u0438 \u043f\u0440\u0435\u0434\u044b\u0434\u0443\u0449\u0435\u0435: <i>v<\/i> \u0438\u043c\u0435\u0435\u0442 \u0442\u0438\u043f <i>SplitView m (concat (split n m xs))<\/i>, \u0430 \u0434\u043e\u043b\u0436\u043d\u043e \u0431\u044b\u0442\u044c <i>SplitView m xs<\/i>. \u041f\u0440\u043e\u0434\u043e\u043b\u0436\u0438\u043c \u043c\u0435\u043d\u044f\u0442\u044c \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435:  <\/p>\n<pre><code class=\"haskell\">splitView n m xs with concat (split n m xs) | [ split n m xs ] splitView n m xs | ys | v = v <\/code><\/pre>\n<p>  \u041a\u043e\u043d\u0441\u0442\u0440\u0443\u043a\u0446\u0438\u044f with \u043c\u043e\u0436\u0435\u0442 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c\u0441\u044f \u0434\u043b\u044f pattern matching&#8217;\u0430 \u0441\u0440\u0430\u0437\u0443 \u043f\u043e \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u0438\u043c \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f\u043c, \u043a\u043e\u0442\u043e\u0440\u044b\u0435 \u043e\u0442\u0434\u0435\u043b\u044f\u044e\u0442\u0441\u044f \u0434\u0440\u0443\u0433 \u043e\u0442 \u0434\u0440\u0443\u0433\u0430 \u0432\u0435\u0440\u0442\u0438\u043a\u0430\u043b\u044c\u043d\u044b\u043c\u0438 \u0447\u0451\u0440\u0442\u043e\u0447\u043a\u0430\u043c\u0438. \u041a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435 with \u043f\u043e\u0440\u043e\u0436\u0434\u0430\u0435\u0442 \u044d\u0444\u0444\u0435\u043a\u0442, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f generalisation. \u041e\u043d \u043f\u0440\u043e\u044f\u0432\u043b\u044f\u0435\u0442\u0441\u044f \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u0442\u0438\u043f\u044b \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u043e\u0432 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u0438 \u0442\u0438\u043f \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f, \u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u043d\u0430\u043c \u043d\u0435\u043e\u0431\u0445\u043e\u0434\u0438\u043c\u043e \u0441\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u043e\u0432\u0430\u0442\u044c, \u043c\u043e\u0433\u0443\u0442 \u043c\u0435\u043d\u044f\u0442\u044c\u0441\u044f \u0432 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u043e\u0441\u0442\u0438 \u043e\u0442 \u0442\u043e\u0433\u043e, \u043f\u043e \u043a\u0430\u043a\u0438\u043c \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f\u043c \u043c\u044b \u0432\u044b\u043f\u043e\u043b\u043d\u044f\u0435\u043c pattern matching \u0441 \u043f\u043e\u043c\u043e\u0449\u044c\u044e with. \u041a \u043f\u0440\u0438\u043c\u0435\u0440\u0443, \u0435\u0441\u043b\u0438 \u0443 \u043d\u0430\u0441 \u0435\u0441\u0442\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u044f  <\/p>\n<pre><code class=\"haskell\">f x y with e f x y | p = ... <\/code><\/pre>\n<p>  \u0442\u043e \u0432 \u0440\u0435\u0437\u0443\u043b\u044c\u0442\u0430\u0442\u0435 generalisation \u0432\u0441\u0435 \u0432\u0445\u043e\u0436\u0434\u0435\u043d\u0438\u044f \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f <i>e<\/i> \u0432 \u0442\u0438\u043f\u044b \u0430\u0440\u0433\u0443\u043c\u0435\u043d\u0442\u043e\u0432 <i>x<\/i> \u0438 <i>y<\/i>, \u0430 \u0442\u0430\u043a \u0436\u0435 \u0432 \u0442\u0438\u043f \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044f, \u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u043d\u0430\u043c \u043d\u0443\u0436\u043d\u043e \u0441\u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u043e\u0432\u0430\u0442\u044c \u0432 \u0442\u0435\u043b\u0435, \u0437\u0430\u043c\u0435\u043d\u044f\u0442\u0441\u044f \u043d\u0430 <i>p<\/i>. \u0410 \u0435\u0441\u043b\u0438 \u0443 \u043d\u0430\u0441 \u0435\u0441\u0442\u044c \u043d\u0435\u0441\u043a\u043e\u043b\u044c\u043a\u043e \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u0439 \u0432 with  <\/p>\n<pre><code class=\"haskell\">f x y with e1 | e2 | e3 f x y | p1 | p2 | p3 = ... <\/code><\/pre>\n<p>  \u0442\u043e, \u043a\u0440\u043e\u043c\u0435 \u0432\u0441\u0435\u0433\u043e \u043f\u0440\u043e\u0447\u0435\u0433\u043e, \u0432\u0441\u0435 \u0432\u0445\u043e\u0436\u0434\u0435\u043d\u0438\u044f <i>e1<\/i> \u0432 <i>p2<\/i> \u0438 <i>p3<\/i> \u0437\u0430\u043c\u0435\u043d\u044f\u0442\u0441\u044f \u043d\u0430 <i>p1<\/i>, \u0432\u0445\u043e\u0436\u0434\u0435\u043d\u0438\u044f <i>e2<\/i> \u0432 <i>p3<\/i> \u0437\u0430\u043c\u0435\u043d\u044f\u0442\u0441\u044f \u043d\u0430 <i>p2<\/i>.<br \/>  \u0412 \u043d\u0430\u0448\u0435\u043c \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0438 <i>splitView<\/i>, \u0431\u043b\u0430\u0433\u043e\u0434\u0430\u0440\u044f \u0434\u043e\u0431\u0430\u0432\u043b\u0435\u043d\u0438\u044e <i>concat (split n m xs)<\/i> \u0432 with \u0442\u0438\u043f <i>v<\/i> \u0438\u0437\u043c\u0435\u043d\u0438\u0442\u0441\u044f \u0441 <i>SplitView m (concat (split n m xs))<\/i> \u043d\u0430 <i>SplitView m ys<\/i>. \u0422\u0435\u043f\u0435\u0440\u044c \u043d\u0430\u043c \u043d\u0430\u0434\u043e \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u044c, \u0447\u0442\u043e <i>xs<\/i> \u0438 <i>ys<\/i> \u2014 \u044d\u0442\u043e \u043e\u0434\u043d\u043e \u0438 \u0442\u043e\u0436\u0435. \u0427\u0442\u043e\u0431\u044b \u044d\u0442\u043e \u0441\u0434\u0435\u043b\u0430\u0442\u044c, \u043d\u0430\u043c \u043f\u043e\u043d\u0430\u0434\u043e\u0431\u0438\u0442\u0441\u044f \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0430\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u044f:  <\/p>\n<pre><code class=\"haskell\">splitConcatLemma : forall {A} -&gt; (n : Nat) -&gt; (m : Nat) -&gt; (xs : Vec A (m * n)) -&gt; concat (split n m xs) == xs <\/code><\/pre>\n<p>  \u041f\u043e \u043f\u0435\u0440\u0435\u0434\u0430\u043d\u043d\u043e\u043c\u0443 \u0432\u0435\u043a\u0442\u043e\u0440\u0443, \u043e\u043d\u0430 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u0443\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0437\u043d\u0430\u043a\u043e\u043c\u043e\u0433\u043e \u043d\u0430\u043c \u0442\u0438\u043f\u0430 <i>==<\/i>, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u0441\u0432\u0438\u0434\u0435\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0443\u0435\u0442 \u043e \u0440\u0430\u0432\u0435\u043d\u0441\u0442\u0432\u0435 \u043d\u0443\u0436\u043d\u044b\u0445 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u0439 <i>concat (split n m xs)<\/i> \u0438 <i>xs<\/i>. \u0418\u0441\u043f\u043e\u043b\u044c\u0437\u0443\u044f \u044d\u0442\u0443 \u0444\u0443\u043d\u043a\u0446\u0438\u044e, \u043f\u043e\u043b\u0443\u0447\u0438\u043c \u0441\u043b\u0435\u0434\u0443\u044e\u0449\u0443\u044e \u0432\u0435\u0440\u0441\u0438\u044e <i>splitView<\/i>:  <\/p>\n<pre><code class=\"haskell\">splitView n m xs with concat (split n m xs) | [ split n m xs ] | splitConcatLemma n m xs splitView n m xs | ys | v | eq = v <\/code><\/pre>\n<p>  \u0417\u0434\u0435\u0441\u044c \u043d\u0438\u043a\u0430\u043a\u0438\u0435 \u0442\u0438\u043f\u044b \u043d\u0435 \u0438\u0437\u043c\u0435\u043d\u0438\u043b\u0438\u0441\u044c, \u043d\u043e <i>eq<\/i> \u0438\u043c\u0435\u0435\u0442 \u0442\u0438\u043f <i>ys == xs<\/i> \u0431\u043b\u0430\u0433\u043e\u0434\u0430\u0440\u044f \u0432\u0441\u0451 \u0442\u043e\u043c\u0443 \u0436\u0435 \u044d\u0444\u0444\u0435\u043a\u0442\u0443 generalisation \u043f\u043e \u043f\u0435\u0440\u0432\u043e\u043c\u0443 \u0432\u044b\u0440\u0430\u0436\u0435\u043d\u0438\u044e \u0432 with. \u0422\u0435\u043f\u0435\u0440\u044c \u0443 \u043d\u0430\u0441 \u0435\u0441\u0442\u044c \u0432\u0441\u0451, \u0447\u0442\u043e\u0431\u044b \u0437\u0430\u0441\u0442\u0430\u0432\u0438\u0442\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u044e \u0440\u0430\u0431\u043e\u0442\u0430\u0442\u044c. \u0412\u044b\u043f\u043e\u043b\u043d\u0438\u043c pattern matching \u043d\u0430 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0438 <i>eq<\/i>:  <\/p>\n<pre><code class=\"haskell\">splitView n m xs with concat (split n m xs) | [ split n m xs ] | splitConcatLemma n m xs splitView n m xs | .xs | v | Refl = v <\/code><\/pre>\n<p>  \u0423\u0440\u0430! \u0422\u0435\u043f\u0435\u0440\u044c \u0432\u0441\u0451 \u0440\u0430\u0431\u043e\u0442\u0430\u0435\u0442!<br \/>  \u042f \u043d\u0435 \u043f\u0440\u0438\u0432\u0451\u043b \u0437\u0434\u0435\u0441\u044c \u043e\u043f\u0440\u0435\u0434\u0435\u043b\u0435\u043d\u0438\u0435 \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <i>splitConcatLemma<\/i>. \u042d\u0442\u043e \u043d\u0435 \u043a\u0440\u0438\u0442\u0438\u0447\u043d\u043e \u0434\u043b\u044f \u043d\u0430\u0448\u0435\u0433\u043e \u0440\u0430\u0437\u0433\u043e\u0432\u043e\u0440\u0430 \u043e \u0448\u0430\u0431\u043b\u043e\u043d\u0435 View, \u043a\u0440\u043e\u043c\u0435 \u0442\u043e\u0433\u043e, \u044f \u0443\u0432\u0435\u0440\u0435\u043d, \u0447\u0442\u043e \u0438 \u0442\u0430\u043a \u0443\u0436\u0435 \u0437\u0430\u0433\u0440\u0443\u0437\u0438\u043b \u0432\u0430\u0441! \u041d\u043e, \u0445\u0440\u0430\u0431\u0440\u044b\u0435 \u0432\u043e\u0438\u043d\u044b, \u0434\u043e\u0447\u0438\u0442\u0430\u0432\u0448\u0438\u0435 \u0434\u043e\u0441\u044e\u0434\u0430, \u043a\u043e\u043d\u0435\u0446 \u043d\u0430 \u0433\u043e\u0440\u0438\u0437\u043e\u043d\u0442\u0435.<br \/>  \u041d\u0430\u043a\u043e\u043d\u0435\u0446, \u0440\u0435\u0430\u043b\u0438\u0437\u0430\u0446\u0438\u044f \u0444\u0443\u043d\u043a\u0446\u0438\u0438 <i>swapAB<\/i> \u0447\u0435\u0440\u0435\u0437 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u0438\u0439 pattern matching \u0441 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c <i>splitView<\/i>:  <\/p>\n<pre><code class=\"haskell\">swapAB : Word 32 -&gt; Word 32 swapAB xs with splitView 8 4 xs swapAB ._ | [ a :: b :: c :: d :: [] ] = concat (b :: a :: c :: d :: []) <\/code><\/pre>\n<h1>\u0417\u0430\u043a\u043b\u044e\u0447\u0435\u043d\u0438\u0435<\/h1>\n<p>  \u041f\u043e\u0441\u043b\u0435 \u043f\u0440\u043e\u0447\u0442\u0435\u043d\u0438\u044f \u0441\u0442\u0430\u0442\u044c\u0438 \u0443 \u0432\u0430\u043c \u043c\u043e\u0433 \u0432\u043e\u0437\u043d\u0438\u043a\u043d\u0443\u0442\u044c \u0432\u043e\u043f\u0440\u043e\u0441: \u0430 \u043d\u0435\u043b\u044c\u0437\u044f \u043b\u0438 \u0442\u0430\u043a\u043e\u0439 \u0436\u0435 \u043f\u043e\u0434\u0445\u043e\u0434 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c \u0432 \u044f\u0437\u044b\u043a\u0430\u0445 \u0431\u0435\u0437 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432? \u0418 \u0434\u0435\u0439\u0441\u0442\u0432\u0438\u0442\u0435\u043b\u044c\u043d\u043e, \u0432\u0441\u0451 \u0447\u0442\u043e \u043c\u044b \u0434\u0435\u043b\u0430\u043b\u0438, \u044d\u0442\u043e \u0437\u0430\u0434\u0430\u0432\u0430\u043b\u0438 \u0442\u0438\u043f \u0434\u0430\u043d\u043d\u044b\u0445, \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u044e\u0449\u0438\u0439 \u043f\u0440\u0435\u0434\u0441\u0442\u0430\u0432\u0438\u0442\u044c \u0438\u0441\u0445\u043e\u0434\u043d\u044b\u0439 \u0442\u0438\u043f \u0432 \u043d\u0443\u0436\u043d\u043e\u043c \u043d\u0430\u043c \u0432\u0438\u0434\u0435, \u0438 \u043f\u0438\u0441\u0430\u043b\u0438 \u0444\u0443\u043d\u043a\u0446\u0438\u044e, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u043f\u043e \u0432\u0445\u043e\u0434\u043d\u043e\u043c\u0443 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044e \u0438\u0441\u0445\u043e\u0434\u043d\u043e\u0433\u043e \u0442\u0438\u043f\u0430 \u043a\u043e\u043d\u0441\u0442\u0440\u0443\u0438\u0440\u0443\u0435\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435 \u0446\u0435\u043b\u0435\u0432\u043e\u0433\u043e.<br \/>  \u041e\u0442\u043b\u0438\u0447\u0438\u0435 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u044f \u0442\u0430\u043a\u043e\u0433\u043e \u043f\u043e\u0434\u0445\u043e\u0434\u0430 \u0432 \u044f\u0437\u044b\u043a\u0430\u0445 \u0431\u0435\u0437 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432 \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u043c\u044b \u0442\u0435\u0440\u044f\u0435\u043c \u0441\u0432\u044f\u0437\u044c \u0441 \u0438\u0441\u0445\u043e\u0434\u043d\u044b\u043c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435\u043c. \u041a \u043f\u0440\u0438\u043c\u0435\u0440\u0443, \u0442\u0438\u043f <i>SnocView<\/i> \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f \u0441\u043f\u0438\u0441\u043a\u0430, \u0434\u043b\u044f \u043a\u043e\u0442\u043e\u0440\u043e\u0433\u043e \u043c\u044b \u0435\u0433\u043e \u0441\u0442\u0440\u043e\u0438\u043c, \u0442\u043e \u0435\u0441\u0442\u044c \u0441\u0432\u044f\u0437\u044c \u043c\u0435\u0436\u0434\u0443 \u0438\u0441\u0445\u043e\u0434\u043d\u044b\u043c \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u0435\u043c \u0438 View \u0441\u043e\u0445\u0440\u0430\u043d\u044f\u0435\u0442\u0441\u044f \u043d\u0430 \u0443\u0440\u043e\u0432\u043d\u0435 \u0442\u0438\u043f\u043e\u0432. \u0417\u0430 \u0441\u0447\u0451\u0442 \u044d\u0442\u043e\u0433\u043e, \u043f\u0440\u0438 \u0432\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0438\u0438 pattern matching \u043d\u0430 \u0437\u043d\u0430\u0447\u0435\u043d\u0438\u044f\u0445 <i>SnocView xs<\/i> \u043c\u044b \u0443\u0437\u043d\u0430\u0451\u043c \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e \u043e \u0442\u043e\u043c, \u043a\u0430\u043a \u0438\u043c\u0435\u043d\u043d\u043e \u0432\u044b\u0433\u043b\u044f\u0434\u0438\u0442 \u0438\u0441\u0445\u043e\u0434\u043d\u044b\u0439 \u0441\u043f\u0438\u0441\u043e\u043a <i>xs<\/i>. \u0411\u0435\u0437 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432 \u043f\u043e\u043b\u0443\u0447\u0430\u0442\u044c \u0442\u0430\u043a\u0443\u044e \u0438\u043d\u0444\u043e\u0440\u043c\u0430\u0446\u0438\u044e \u043d\u0435 \u043f\u043e\u043b\u0443\u0447\u0438\u0442\u0441\u044f.<br \/>  \u0412\u0442\u043e\u0440\u043e\u0435 \u043e\u0442\u043b\u0438\u0447\u0438\u0435, \u0432\u044b\u0442\u0435\u043a\u0430\u044e\u0449\u0435\u0435 \u0438\u0437 \u043f\u0435\u0440\u0432\u043e\u0433\u043e, \u0437\u0430\u043a\u043b\u044e\u0447\u0430\u0435\u0442\u0441\u044f \u0432 \u0442\u043e\u043c, \u0447\u0442\u043e \u0431\u0435\u0437 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432, \u0444\u0443\u043d\u043a\u0446\u0438\u044f, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0441\u0442\u0440\u043e\u0438\u0442 View, \u0431\u0443\u0434\u0435\u0442 \u0441\u043b\u0438\u0448\u043a\u043e\u043c \u043e\u0431\u0449\u0435\u0439. \u041a \u043f\u0440\u0438\u043c\u0435\u0440\u0443, \u0444\u0443\u043d\u043a\u0446\u0438\u044f <i>snocView<\/i> \u0438\u043c\u0435\u0435\u0442 \u0442\u0438\u043f:  <\/p>\n<pre><code class=\"haskell\">snocView : {A : Set} -&gt; (xs : List A) -&gt; SnocView xs <\/code><\/pre>\n<p>  \u0418\u0437 \u043d\u0435\u0433\u043e \u044f\u0441\u043d\u043e, \u0447\u0442\u043e \u0442\u0435\u043b\u043e \u0444\u0443\u043d\u043a\u0446\u0438\u0438 \u043d\u0435 \u043c\u043e\u0436\u0435\u0442 \u0431\u044b\u0442\u044c \u0441\u043e\u0432\u0435\u0440\u0448\u0435\u043d\u043d\u043e \u043f\u0440\u043e\u0438\u0437\u0432\u043e\u043b\u044c\u043d\u044b\u043c \u2014 \u043e\u043d\u043e \u043e\u0433\u0440\u0430\u043d\u0438\u0447\u0435\u043d\u043d\u043e \u0442\u0435\u043c \u0444\u0430\u043a\u0442\u043e\u043c, \u0447\u0442\u043e <i>SnocView<\/i> \u0437\u0430\u0432\u0438\u0441\u0438\u0442 \u043e\u0442 <i>xs<\/i>. \u0415\u0441\u043b\u0438 \u0431\u044b \u0443 \u043d\u0430\u0441 \u043d\u0435 \u0431\u044b\u043b\u043e \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u0445 \u0442\u0438\u043f\u043e\u0432, \u0442\u043e \u044d\u0442\u0430 \u0444\u0443\u043d\u043a\u0446\u0438\u044f \u043c\u043e\u0433\u043b\u0430 \u0431\u044b \u0438\u043c\u0435\u0442\u044c \u0442\u0438\u043f  <\/p>\n<pre><code class=\"haskell\">snocView : List A -&gt; SnocView <\/code><\/pre>\n<p>  \u0438, \u0441\u043a\u0430\u0436\u0435\u043c, \u043f\u0440\u043e\u0441\u0442\u043e \u0432\u043e\u0437\u0432\u0440\u0430\u0449\u0430\u0442\u044c \u043f\u0443\u0441\u0442\u043e\u0439 \u0441\u043f\u0438\u0441\u043e\u043a \u043d\u0430 \u043b\u044e\u0431\u043e\u043c \u0432\u0445\u043e\u0434\u0435, \u0447\u0442\u043e \u0434\u0435\u043b\u0430\u0435\u0442 \u0435\u0451 \u0434\u043e\u0441\u0442\u0430\u0442\u043e\u0447\u043d\u043e \u0431\u0435\u0441\u043f\u043e\u043b\u0435\u0437\u043d\u043e\u0439.<\/p>\n<p>  \u041f\u043e\u044d\u0442\u043e\u043c\u0443, \u0437\u0430\u043a\u043e\u043d\u0447\u0443 \u0441\u0432\u043e\u0439 \u043f\u043e\u0441\u0442 \u0441\u043b\u043e\u0432\u0430\u043c\u0438, \u0441 \u043a\u043e\u0442\u043e\u0440\u044b\u0445 \u043d\u0430\u0447\u0438\u043d\u0430\u0435\u0442\u0441\u044f \u0441\u0442\u0430\u0442\u044c\u044f The Power Of Pi: dependent types matter!<\/p>\n<p>  <i>\u0421\u0441\u044b\u043b\u043a\u0438:<\/i><br \/>  <a href=\"http:\/\/cs.ru.nl\/~wouters\/Publications\/ThePowerOfPi.pdf\">Nicolas Oury, Wouter Swierstra \u00abThe Power Of Pi\u00bb<\/a><br \/>  <a href=\"http:\/\/agda.readthedocs.org\/en\/latest\/language\/with-abstraction.html\">\u0414\u043e\u043a\u0443\u043c\u0435\u043d\u0442\u0430\u0446\u0438\u044f \u043f\u043e with<\/a><br \/>  <a href=\"https:\/\/github.com\/octomarat\/AgdaLearning\/tree\/master\/ThePowerOfPi\/ViewHabraPaper\/src\">\u0418\u0441\u0445\u043e\u0434\u043d\u0438\u043a\u0438<\/a>               <\/p>\n<div class=\"clear\"><\/div>\n<p> \u0441\u0441\u044b\u043b\u043a\u0430 \u043d\u0430 \u043e\u0440\u0438\u0433\u0438\u043d\u0430\u043b \u0441\u0442\u0430\u0442\u044c\u0438 <a href=\"https:\/\/habrahabr.ru\/post\/277989\/\"> https:\/\/habrahabr.ru\/post\/277989\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>       <img decoding=\"async\" src=\"https:\/\/habrastorage.org\/files\/0e0\/67b\/a24\/0e067ba244494c62b8f4941c4898ba60.jpg\"\/><\/p>\n<p>  \u0428\u0430\u0431\u043b\u043e\u043d\u044b \u043f\u0440\u043e\u0435\u043a\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f! \u0412\u043f\u0435\u0440\u0432\u044b\u0435 \u044f \u0443\u0437\u043d\u0430\u043b \u043e \u043d\u0438\u0445 \u043d\u0430 \u043a\u0443\u0440\u0441\u0435 Software Design, \u043a\u043e\u0433\u0434\u0430 \u0443\u0447\u0438\u043b\u0441\u044f \u0432 \u043c\u0430\u0433\u0438\u0441\u0442\u0440\u0430\u0442\u0443\u0440\u0435 \u0410\u043a\u0430\u0434\u0435\u043c\u0438\u0447\u0435\u0441\u043a\u043e\u0433\u043e \u0443\u043d\u0438\u0432\u0435\u0440\u0441\u0438\u0442\u0435\u0442\u0430. \u041c\u044b \u043f\u0438\u0441\u0430\u043b\u0438 \u0440\u0430\u0437\u043b\u0438\u0447\u043d\u044b\u0435 \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u044b \u043d\u0430 Java \u0441 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u043d\u0438\u0435\u043c \u0448\u0430\u0431\u043b\u043e\u043d\u043e\u0432. \u0421 \u0442\u0435\u0445 \u043f\u043e\u0440 \u044d\u0442\u043e \u0441\u043b\u043e\u0432\u043e\u0441\u043e\u0447\u0435\u0442\u0430\u043d\u0438\u0435 \u0430\u0441\u0441\u043e\u0446\u0438\u0438\u0440\u0443\u0435\u0442\u0441\u044f \u0443 \u043c\u0435\u043d\u044f \u0441 \u0447\u0435\u043c-\u0442\u043e \u0442\u0430\u043a\u0438\u043c \u041e\u041e\u041f\u0448\u043d\u044b\u043c. \u041e\u0434\u043d\u0430\u043a\u043e, \u0440\u0430\u0437\u0431\u0438\u0440\u0430\u044f\u0441\u044c \u0441 \u044f\u0437\u044b\u043a\u043e\u043c Agda, \u044f \u043d\u0430\u0442\u043a\u043d\u0443\u043b\u0441\u044f \u043d\u0430 \u0441\u0442\u0430\u0442\u044c\u044e The Power Of Pi, \u043a\u043e\u0442\u043e\u0440\u0430\u044f \u0440\u0430\u0441\u0441\u043a\u0430\u0437\u044b\u0432\u0430\u0435\u0442 \u043f\u0440\u043e \u0448\u0430\u0431\u043b\u043e\u043d\u044b \u043f\u0440\u043e\u0435\u043a\u0442\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0432 \u044f\u0437\u044b\u043a\u0430\u0445 \u0441 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438!<\/p>\n<p>  \u0412 \u044d\u0442\u043e\u043c \u043f\u043e\u0441\u0442\u0435 \u044f \u0445\u043e\u0447\u0443 \u0440\u0430\u0441\u0441\u043a\u0430\u0437\u0430\u0442\u044c \u043e\u0431 \u043e\u0434\u043d\u043e\u043c \u0438\u0437 \u044d\u0442\u0438\u0445 \u0448\u0430\u0431\u043b\u043e\u043d\u043e\u0432, \u043a\u043e\u0442\u043e\u0440\u044b\u0439 \u043d\u0430\u0437\u044b\u0432\u0430\u0435\u0442\u0441\u044f View. \u0421 \u0435\u0433\u043e \u043f\u043e\u043c\u043e\u0449\u044c\u044e \u043c\u043e\u0436\u043d\u043e \u0440\u0435\u0430\u043b\u0438\u0437\u043e\u0432\u044b\u0432\u0430\u0442\u044c \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u0438\u0435 \u043f\u0440\u0430\u0432\u0438\u043b\u0430 pattern matching&#8217;a. \u0415\u0441\u043b\u0438 \u0432\u0430\u043c \u0438\u043d\u0442\u0435\u0440\u0435\u0441\u043d\u043e, \u0447\u0442\u043e \u044d\u0442\u043e \u0437\u0430 \u0448\u0430\u0431\u043b\u043e\u043d, \u0447\u0442\u043e \u0442\u0430\u043a\u043e\u0435 \u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u0435\u043b\u044c\u0441\u043a\u0438\u0439 pattern matching, \u043a\u0430\u043a\u043e\u0432\u044b \u043e\u0441\u043e\u0431\u0435\u043d\u043d\u043e\u0441\u0442\u0438 pattern matching&#8217;\u0430 \u0432 \u044f\u0437\u044b\u043a\u0430\u0445 \u0441 \u0437\u0430\u0432\u0438\u0441\u0438\u043c\u044b\u043c\u0438 \u0442\u0438\u043f\u0430\u043c\u0438, \u0438 \u0432\u044b \u0437\u043d\u0430\u043a\u043e\u043c\u044b \u0441 \u043a\u0430\u043a\u0438\u043c-\u043d\u0438\u0431\u0443\u0434\u044c \u0444\u0443\u043d\u043a\u0446\u0438\u043e\u043d\u0430\u043b\u044c\u043d\u044b\u043c \u044f\u0437\u044b\u043a\u043e\u043c \u043f\u0440\u043e\u0433\u0440\u0430\u043c\u043c\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u044f \u0441\u043e \u0441\u0442\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0442\u0438\u043f\u0438\u0437\u0430\u0446\u0438\u0435\u0439 (Haskell, Scala, Ocaml, F#) \u2014 \u0434\u043e\u0431\u0440\u043e \u043f\u043e\u0436\u0430\u043b\u043e\u0432\u0430\u0442\u044c \u043f\u043e\u0434 \u043a\u0430\u0442!<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"class_list":["post-274981","post","type-post","status-publish","format-standard","hentry"],"_links":{"self":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/274981","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=274981"}],"version-history":[{"count":0,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=\/wp\/v2\/posts\/274981\/revisions"}],"wp:attachment":[{"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=274981"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=274981"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/savepearlharbor.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=274981"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}