{"id":395,"date":"2017-11-20T06:53:23","date_gmt":"2017-11-19T22:53:23","guid":{"rendered":"https:\/\/colliot.me\/?p=395"},"modified":"2017-11-22T18:11:28","modified_gmt":"2017-11-22T10:11:28","slug":"what-is-gadt-in-haskell","status":"publish","type":"post","link":"https:\/\/colliot.org\/ru\/2017\/11\/what-is-gadt-in-haskell\/","title":{"rendered":"(\u4e2d\u6587) \u4ec0\u4e48\u662f Haskell \u4e2d\u7684 GADT\uff08\u5e7f\u4e49\u4ee3\u6570\u6570\u636e\u7c7b\u578b\uff09\uff1f"},"content":{"rendered":"<p class=\"qtranxs-available-languages-message qtranxs-available-languages-message-ru\">\u0418\u0437\u0432\u0438\u043d\u0438\u0442\u0435, \u044d\u0442\u043e\u0442 \u0442\u0435\u0445\u0442 \u0434\u043e\u0441\u0442\u0443\u043f\u0435\u043d \u0442\u043e\u043b\u044c\u043a\u043e \u0432 &ldquo;<a href=\"https:\/\/colliot.org\/zh\/wp-json\/wp\/v2\/posts\/395\" class=\"qtranxs-available-language-link qtranxs-available-language-link-zh\" title=\"\u4e2d\u6587\">\u4e2d\u6587<\/a>&rdquo; \u0438 &ldquo;<a href=\"https:\/\/colliot.org\/en\/wp-json\/wp\/v2\/posts\/395\" class=\"qtranxs-available-language-link qtranxs-available-language-link-en\" title=\"English\">\u0410\u043c\u0435\u0440\u0438\u043a\u0430\u043d\u0441\u043a\u0438\u0439 \u0410\u043d\u0433\u043b\u0438\u0439\u0441\u043a\u0438\u0439<\/a>&rdquo;. For the sake of viewer convenience, the content is shown below in this site default language. You may click one of the links to switch the site language to another available language.<\/p><p>\u5148\u770b\u770b\u6ca1\u6709 GADT \u7684\u65f6\u5019\u6211\u4eec\u5728\u505a\u5565\u3002\u6700\u7b80\u5355\u7684\uff0c\u6bd4\u5982\u5b9a\u4e49\u4e00\u4e2a\u5217\u8868\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">List a = Nil | Cons a (List a)<\/pre>\n<p>\u5b83\u662f\u5728\u505a\u5565\u5462\uff1f<\/p>\n<ul>\n<li>\u5148\u770b\u7b49\u53f7\u5de6\u8fb9\uff0c\u5b83\u9996\u5148\u5b9a\u4e49\u4e86\u4e00\u4e2a\u53eb List \u7684 type constructor\uff0c\u5b83\u63a5\u53d7\u4e00\u4e2a\u7c7b\u578b\uff0c\u5e76\u8fd4\u56de\u4e00\u4e2a\u65b0\u7684\u7c7b\u578b\u3002\u5176\u5b9e\u5c31\u662f\u7c7b\u578b\u7684\u51fd\u6570\u3002<\/li>\n<li>\u518d\u770b\u53f3\u8fb9\uff0c\u5b83\u544a\u8bc9\u6211\u4eec\u6709\u4e24\u79cd\u65b9\u5f0f\u83b7\u5f97\u4e00\u4e2a\u7c7b\u578b\u4e3a List a \u7684\u503c\uff0c\u4e00\u4e2a\u53eb Nil\uff0c\u4e00\u4e2a\u53eb Cons a (List a)\u3002\n<ul>\n<li>Nil \u7684\u8bdd\uff0c\u4f60\u76f4\u63a5\u5199 Nil\uff0c\u5b83\u5c31\u662f\u4e00\u4e2a List a \u7c7b\u578b\u7684\u503c\uff0c\u81f3\u4e8e\u8fd9\u4e2a a \u5177\u4f53\u662f\u5565\uff0c\u9700\u8981\u7ed3\u5408\u4e0a\u4e0b\u6587\u63a8\u5bfc\u624d\u77e5\u9053\u3002<\/li>\n<li>\u800c Cons a (List a) \u5462\uff0c\u5b83\u662f\u63a5\u53d7\u4e24\u4e2a\u53c2\u6570\uff0c\u4e00\u4e2a\u7c7b\u578b\u662f a\uff0c\u4e00\u4e2a\u7c7b\u578b\u662f List a\uff0c\u7136\u540e\u8fd4\u56de\u4e00\u4e2a List a \u7c7b\u578b\u7684\u503c\u3002\u81f3\u4e8e\u8fd9\u4e2a a \u662f\u5565\uff0c\u6211\u4eec\u540c\u6837\u662f\u9700\u8981\u63a8\u5bfc\u624d\u80fd\u77e5\u9053\u7684\uff0c\u4e0d\u8fc7\u662f\u8fd9\u91cc\u7684\u63a8\u5bfc\u6bd4\u8f83\u663e\u8457\u7f62\u4e86\uff0c\u56e0\u4e3a\u76f4\u63a5\u5c31\u662f\u7b2c\u4e00\u4e2a\u53c2\u6570\u7684\u7c7b\u578b\u3002<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>\u90a3\u4e48\u6211\u4eec\u53ef\u4ee5\u7528\u51fd\u6570\u5f62\u5f0f\u7ed9\u8fd9\u4fe9\u8868\u793a\u51fa\u6765\uff1a<!--more--><\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">Nil :: List a\r\nCons :: a -&gt; List a -&gt; List a<\/pre>\n<p>\u53ef\u4ee5\u770b\u5230\u5b83\u4eec\u63a5\u53d7\u4e00\u4e9b\u53c2\u6570\uff0c\u4f46\u8fd4\u56de\u7c7b\u578b\u90fd\u662f List a\u3002<b>GADT \u552f\u4e00\u6539\u7684\u5c31\u662f\u8fd4\u56de\u7c7b\u578b\u8fd9\u4e2a\u5730\u65b9<\/b>\uff0c\u6211\u4eec\u4e0d\u4e00\u5b9a\u5fc5\u987b\u5199 a\uff0c\u800c\u662f\u53ef\u4ee5\u628a a \u66ff\u6362\u4e3a\u53e6\u5916\u7684\u7c7b\u578b\u3002\u6bd4\u5982\u8bf4\u6211\u4eec\u53ef\u4ee5\u6709\u4e00\u4e2a\u53ea\u80fd\u4f5c\u4e3a Int \u5217\u8868\u7684\u5934\u7684\u6784\u9020\u51fd\u6570\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">IntNil :: List Int<\/pre>\n<p>\u6211\u4eec\u53ef\u4ee5\u8bd5\u9a8c\u4e00\u4e0b\uff08\u8fd9\u4e2a\u5c31\u662f GADT \u7684\u5199\u6cd5\u4e86\uff09\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">data List a where\r\n  IntNil :: List Int\r\n  Nil :: List a\r\n  Cons :: a -&gt; List a -&gt; List a\r\n\r\na :: List Int\r\na = IntNil\r\n\r\n-- \u4f1a\u62a5\u9519\uff0c\u56e0\u4e3a\u7c7b\u578b\u4e0d\u76f8\u5bb9\r\n-- c_ :: List Char\r\n-- c_ = IntNil\r\n\r\n-- \u8fd9\u4e2a\u5c31\u662f\u76f8\u5bb9\u7684\r\nc :: List Char\r\nc = Nil<\/pre>\n<p>\u5f53\u7136\u5de6\u8fb9\u4e0d\u4e00\u5b9a\u5f97\u662f List Int \u8fd9\u6837\u76f4\u767d\u7684\u7c7b\u578b\uff0c\u53ea\u8981\u662f\u4e00\u4e2a\u5f62\u5982 List \u7684\u7c7b\u578b\u5c31\u53ef\u4ee5\u4e86\uff0c\u4f60\u751a\u81f3\u53ef\u4ee5\u628a\u81ea\u5df1\u5d4c\u5957\u8fdb\u53bb\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">data Pair a b where Pair :: a -&gt; b -&gt; Pair a b\r\n\r\ndata List a where IntListNil :: List (List Int)\r\n  ListNil :: List (List a)\r\n  IntNil :: List Int\r\n  Nil :: List a\r\n  Cons :: a -&gt; List a -&gt; List a\r\n  -- \u8fd9\u4e2a\u5c31\u4e0d\u884c\uff0c\u56e0\u4e3a\u5f62\u5982 Pair \u800c\u4e0d\u662f List\r\n  -- Bad :: a -&gt; List a -&gt; Pair a (List a)<\/pre>\n<p>\u90a3\u4e48\u5b83\u53ef\u4ee5\u5e72\u5565\u7528\u5462\uff1f\u6211\u6240\u77e5\u9053\u7684\u6709\u8fd9\u4e48\u4e00\u4e9b\uff08\u90fd\u4e0d\u8d85\u51fa\u7f51\u4e0a\u7684 wiki \u7684\u8303\u7574\uff09\uff1a<\/p>\n<p>\u4e00\u79cd\u5c31\u662f\u6700\u6709\u540d\u7684\uff0c\u5d4c\u5165\u4e00\u79cd\u8bed\u8a00\uff08\u7684\u8bed\u6cd5\u6811\uff09\u3002\u6bd4\u5982\u8fd9\u4e48\u4e00\u79cd\u7b80\u5355\u7684\u8868\u8fbe\u5f0f\u8bed\u8a00\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">data Expr = \r\n    ILit Int\r\n  | BLit Bool\r\n  | Add Expr Expr\r\n  | Eq Expr Expr<\/pre>\n<p>\u8fd9\u6837\u662f\u8db3\u591f\u8868\u8fbe\u4e86\uff0c\u4f46\u662f\u5b58\u5728\u4e00\u4e9b\u95ee\u9898\u2014\u2014\u6bd4\u5982\u6211\u4eec\u4e0d\u5e0c\u671b Bool \u88ab Add\uff08\u5c31\u662f\u8bf4\u6211\u4eec\u8981\u5d4c\u5165\u7684\u8bed\u8a00\uff0c\u5b83\u672c\u8eab\u4e5f\u662f\u6709\u7c7b\u578b\u7684\uff0c\u6709\u4e9b\u8fd0\u7b97\u4e0d\u80fd\u5bf9\u67d0\u4e9b\u5bf9\u8c61\u505a\uff09\uff0c\u4f46\u8fd9\u4e2a\u5b9a\u4e49\u65e0\u6cd5\u907f\u514d\u6211\u4eec\u5199\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">addBool :: Expr\r\naddBool = Add (BLit True) (BLit False)<\/pre>\n<p>\u4e00\u4e2a\u60f3\u6cd5\u662f\u628a\u8fd9\u4e2a Expr \u7684\u300c\u8fd4\u56de\u503c\u300d\u7c7b\u578b\u8bb0\u5f55\u4e0b\u6765\uff0c\u5c31\u50cf\u6211\u4eec\u5bf9 List \u505a\u7684\u90a3\u6837\uff08\u5728\u90a3\u91cc\u6211\u4eec\u8bb0\u5f55\u7684\u662f\u6210\u5458\u7c7b\u578b\uff09\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">data Expr a = \r\n    ILit Int\r\n  | BLit Bool\r\n  | Add (Expr Int) (Expr Int)\r\n  | Eq (Expr a) (Expr a)<\/pre>\n<p>\u8fd9\u4e2a\u770b\u8d77\u6765\u5f88\u7f8e\u597d\uff0c\u4f46\u662f\u884c\u4e0d\u884c\u5462\uff1f<\/p>\n<p>\u5b9e\u9645\u4e0a\u662f\u4e0d\u884c\u7684\uff01\u4f60\u4e0d\u8981\u4ee5\u4e3a BLit True \u5c31\u662f Expr Bool \u7c7b\u578b\uff0c\u4ece\u800c\u4f1a\u4e0d\u80fd\u4f5c\u4e3a Add \u7684\u53c2\u6570\u4e86\u3002\u5176\u5b9e\uff0c\u8fd9\u91cc\u7684 BLit True \u8fd8\u662f Expr a \u7c7b\u578b\uff0c\u5176\u4e2d a \u662f\u4efb\u610f\u7c7b\u578b\uff0c\u5c31\u50cf\u4e4b\u524d\u7684 Nil \u662f List a \u7c7b\u578b\u3001a \u662f\u4efb\u610f\u7684\u4e00\u6837\u3002<\/p>\n<p>\u8fd9\u4e2a\u65f6\u5019\u5c31\u4f53\u73b0\u51fa GADT \u7684\u91cd\u8981\u6027\u4e86\u2014\u2014\u53ea\u6709\u900f\u8fc7 GADT \u624d\u80fd\u9650\u5b9a\u4e00\u4e2a\u300c\u6784\u9020\u51fd\u6570\u300d\u7684\u8fd4\u56de\u7c7b\u578b\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">data Expr a where\r\n  ILit :: Int -&gt; Expr Int\r\n  BLit :: Bool -&gt; Expr Bool\r\n  Add :: Expr Int -&gt; Expr Int -&gt; Expr Int\r\n  -- \u5bf9 Eq \u6211\u4eec\u53ef\u4ee5\u653e\u5bbd\u8981\u6c42\uff0c\u53ea\u7528 typeclass \u6765\u9650\u5236\uff0c\u4e0d\u5fc5\u6307\u5b9a\u5177\u4f53\u7c7b\u578b\r\n  Eq :: Eq a =&gt; Expr a -&gt; Expr a -&gt; Expr Bool<\/pre>\n<p>\u8fd9\u65f6\u5019\u5b83\u5c31\u80fd\u5206\u8fa8\u662f\u975e\u4e86\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">-- \u62a5\u9519\uff0c\u56e0\u4e3a Expr Bool \u548c Expr Int \u4e0d\u517c\u5bb9\r\n-- addBool =  Add (BLit True) (BLit False)\r\naddInt = Add (ILit 1) (ILit 2)\r\neqBool = Eq (BLit True) (BLit False)<\/pre>\n<p>\u5f88\u7f8e\u5999\uff0c\u662f\u4e0d\u662f\uff1f<\/p>\n<p>\u8fd9\u5c31\u662f\u6240\u8c13\u7684 initial embedding of a language\uff0c\u800c\u6211\u4eec\u6700\u540e\u5f97\u5230\u7684\u7528 GADT \u7684\u7248\u672c\uff0c\u53eb tagless initial embedding\u3002\u4e3a\u4ec0\u4e48\u662f tagless \u5462\uff1f\u56e0\u4e3a\u539f\u59cb\u7684 ADT \u662f\u6240\u8c13\u7684 \u201ctagged union\u201d\u3002\u6211\u4eec\u73b0\u5728\u629b\u5f03\u4e86\u5b83\uff0c\u6240\u4ee5\u53eb tagless\u3002<\/p>\n<p>\u8fd9\u4e2a Expr \u662f\u5f88\u7b80\u5355\u7684\u8bed\u8a00\u3002\u5b9e\u9645\u4e0a\u4f60\u5b8c\u5168\u53ef\u4ee5\u5c06 simply typed lambda calculus \u7ed9\u8fd9\u6837\u5d4c\u5165\u8fdb\u53bb\u3002<\/p>\n<p>\u76f8\u5bf9\u4e8e initial embedding\uff0c\u6211\u4eec\u8fd8\u53ef\u4ee5\u6709\u6240\u8c13 final embedding\uff0c\u4e0d\u8fc7\u8ddf GADT \u5173\u7cfb\u4e0d\u5927\u4e86\u3002<\/p>\n<hr \/>\n<p>\u6211\u4eec\u8fd8\u53ef\u4ee5\u73a9\u70b9\u66f4\u98ce\u9a9a\u7684\u3002\u6bd4\u5982\u8fd9\u91cc\u5047\u5982\u6709\u4e00\u79cd\u7b80\u5355\u7684\u3001\u63cf\u8ff0\u6808\u64cd\u4f5c\u7684\u8bed\u8a00\uff0cPush \u8868\u793a\u63a8\u5165\u4e00\u4e2a\u6570\uff0cAdd \u8868\u793a\u5f39\u51fa\u4e24\u4e2a\u6570\uff0c\u628a\u5b83\u4eec\u7684\u548c\u63a8\u56de\u53bb\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">data StackLang where\r\n  Begin :: StackLang\r\n  Push :: Int -&gt; StackLang -&gt; StackLang\r\n  Add :: StackLang -&gt; StackLang\r\n\r\nbug = Add (Push 1 Begin)<\/pre>\n<p>\u8fd9\u91cc\u7684 bug \u8bed\u53e5\u5b9e\u9645\u4e0a\u662f\u6709 bug \u7684\uff0c\u56e0\u4e3a\u4f60\u521a\u63a8\u8fdb\u53bb\u4e00\u4e2a 1\uff0c\u6ca1\u6709\u4eba\u548c\u5b83\u76f8\u52a0\u3002\u90a3\u4e48\u80fd\u4e0d\u80fd\u4ece\u7c7b\u578b\u5c42\u9762\u6765\u6d88\u9664\u8fd9\u79cd bug\u5462\uff1f<\/p>\n<p>\u6211\u4eec\u60f3\uff0c\u8981\u662f StackLang \u7684\u7c7b\u578b\u91cc\u9762\uff0c\u5e26\u4e0a\u6808\u91cc\u6709\u591a\u5c11\u4e2a\u6570\u8be5\u591a\u597d\u554a\uff01\u4f46\u662f\u8fd9\u65f6\u5019 Begin \u5c31\u4e0d\u80fd\u8fd4\u56de\u4e00\u822c\u7684 StackLang \u7c7b\u578b\u4e86\uff0c\u800c\u662f\u5e26\u6709 0 \u4e2a\u6570\u7684 StackLang \u7c7b\u578b\uff0c\u540c\u7406\uff0cPush \u63a5\u53d7\u5e26\u6709 n \u4e2a\u6570\u7684 StackLang \u7c7b\u578b\uff0c\u8fd4\u56de\u5e26\u6709 n+1 \u4e2a\u6570\u7684 StackLang \u7c7b\u578b\uff0cAdd \u5219\u662f n+2 -&gt; n+1\u3002\u6b64\u65f6 GADT \u5c31\u53ef\u4ee5\u6d3e\u4e0a\u7528\u573a\u4e86\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">data Z\r\ndata S n\r\n\r\ndata SStackLang t where\r\n  SBegin :: SStackLang Z\r\n  SPush :: Int -&gt; SStackLang t -&gt; SStackLang (S t)\r\n  SAdd :: SStackLang (S (S t)) -&gt; SStackLang (S t)<\/pre>\n<p>\u8fd9\u91cc Z \u548c S \u5c31\u662f\u5bf9\u81ea\u7136\u6570\u7684 0 \u548c\u540e\u7ee7\uff08successor\uff09\u7684\u6a21\u62df\u3002\u8fd9\u65f6\u5019\u4f60\u4f1a\u53d1\u73b0\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">sBug = SAdd (SPush 1 SBegin)<\/pre>\n<p>\u4f1a\u62a5\u9519<\/p>\n<blockquote><p>\u2022 Couldn\u2019t match type \u2018Z\u2019 with \u2018S t\u2019<br \/>\nExpected type: SStackLang (S (S t))<br \/>\nActual type: SStackLang (S Z)<\/p><\/blockquote>\n<p>\u975e\u5e38\u5b89\u5168\u3002<\/p>\n<p>\u5176\u5b9e\u8fd9\u5c31\u662f\u5bf9\u6240\u8c13\u7684\u300c\u4f9d\u8d56\u7c7b\u578b\u300d(dependent type) \u7684\u6a21\u62df\u3002\u4eff\u7167\u8fd9\u4e2a\u4f60\u8fd8\u53ef\u4ee5\u9020\u51fa\u300c\u957f\u5ea6\u4e3a n\u300d\u7684\u5217\u8868\u7684\u6982\u5ff5\uff0c\u5e76\u5bf9\u5176\u5b9a\u4e49\u5b89\u5168\u7684\u64cd\u4f5c\u3002\u8fd9\u5c31\u662f\u540e\u8bdd\u4e86\u3002<\/p>\n<hr \/>\n<p>GADT \u8fd8\u53ef\u4ee5\u628a type \u8f6c\u5316\u4e3a value\u3002\u628a\u7c7b\u578b\u4fdd\u5b58\u5728\u4e00\u4e2a\u503c\u91cc\uff0c\u672c\u6765\u4f60\u56fa\u7136\u662f\u53ef\u4ee5\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">data Witness a = Witness a<\/pre>\n<p>\u4f46\u8fd9\u6837\u4f60\u5f97\u63d0\u4f9b\u4e00\u4e2a a \u7c7b\u578b\u7684\u503c\u624d\u80fd\u628a\u7c7b\u578b\u8bb0\u5f55\u8fdb\u53bb\u3002\u4e00\u65b9\u9762\u5f88\u591a\u65f6\u5019\u6ca1\u6cd5\u6784\u9020\u8fd9\u4e2a\u503c\uff0c\u53e6\u4e00\u65b9\u9762\u53ef\u80fd\u6709\u7684\u7c7b\u578b\u5c31\u6ca1\u6709\u503c\uff0c\u6700\u540e\u8981\u6c42\u63d0\u4f9b\u503c\u7684\u505a\u6cd5\u6839\u672c\u5c31\u662f\u4e0d\u79d1\u5b66\u7684\u3002<\/p>\n<p>\u4f46\u662f\u6709 GADT \u4f60\u5c31\u53ef\u4ee5\u4e3a\u6240\u6b32\u4e3a\u2014\u2014\u6211\u4e0d\u4e00\u5b9a\u8981\u63a5\u53d7\u4e00\u4e2a\u503c\uff0c\u624d\u80fd\u5f97\u5230\u8fd9\u4e2a\u7c7b\u578b\u4e86\uff1a<\/p>\n<pre class=\"prettyprint lang-haskell\" data-start-line=\"1\" data-visibility=\"visible\" data-highlight=\"\" data-caption=\"\">data Witness a where\r\n  IntWitness :: Witness Int\r\n  BoollWitness :: Witness Bool<\/pre>\n<p>\u8fd9\u5c31\u662f\u6240\u8c13\u7684 \u201ctype witness\u201d\u3002\u81f3\u4e8e\u8fd9\u4e2a\u6709\u4ec0\u4e48\u7528\uff0c\u600e\u4e48\u7528\uff0c\u4e3a\u4ec0\u4e48\u8981\u8fd9\u4e48\u7528\uff0c\uff08\u5f85\u7eed\uff09\u3002<\/p>","protected":false},"excerpt":{"rendered":"<p>\u0418\u0437\u0432\u0438\u043d\u0438\u0442\u0435, \u044d\u0442\u043e\u0442 \u0442\u0435\u0445\u0442 \u0434\u043e\u0441\u0442\u0443\u043f\u0435\u043d \u0442\u043e\u043b\u044c\u043a\u043e \u0432 &ldquo;\u4e2d\u6587&rdquo;. For the sake of viewer convenience, the content is shown below in the alternative language. You may click the link to switch the active language.\u5148\u770b\u770b\u6ca1\u6709 GADT \u7684\u65f6\u5019\u6211\u4eec\u5728\u505a\u5565\u3002\u6700\u7b80\u5355\u7684\uff0c\u6bd4\u5982\u5b9a\u4e49\u4e00\u4e2a\u5217\u8868\uff1a List a = Nil | Cons a (List a) \u5b83\u662f\u5728\u505a\u5565\u5462\uff1f \u5148\u770b\u7b49\u53f7\u5de6\u8fb9\uff0c\u5b83\u9996\u5148\u5b9a\u4e49\u4e86\u4e00\u4e2a\u53eb List \u7684 type constructor\uff0c\u5b83\u63a5\u53d7\u4e00\u4e2a\u7c7b\u578b\uff0c\u5e76\u8fd4\u56de\u4e00\u4e2a\u65b0\u7684\u7c7b\u578b\u3002\u5176\u5b9e\u5c31\u662f\u7c7b\u578b\u7684\u51fd\u6570\u3002 \u518d\u770b\u53f3\u8fb9\uff0c\u5b83\u544a\u8bc9\u6211\u4eec\u6709\u4e24\u79cd\u65b9\u5f0f\u83b7\u5f97\u4e00\u4e2a\u7c7b\u578b\u4e3a List a \u7684\u503c\uff0c\u4e00\u4e2a\u53eb Nil\uff0c\u4e00\u4e2a\u53eb Cons &hellip; <a href=\"https:\/\/colliot.org\/ru\/2017\/11\/what-is-gadt-in-haskell\/\" class=\"more-link\">Continue reading<span class=\"screen-reader-text\"> &#171;(\u4e2d\u6587) \u4ec0\u4e48\u662f Haskell \u4e2d\u7684 GADT\uff08\u5e7f\u4e49\u4ee3\u6570\u6570\u636e\u7c7b\u578b\uff09\uff1f&#187;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[16],"tags":[34,32],"_links":{"self":[{"href":"https:\/\/colliot.org\/ru\/wp-json\/wp\/v2\/posts\/395"}],"collection":[{"href":"https:\/\/colliot.org\/ru\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/colliot.org\/ru\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/colliot.org\/ru\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/colliot.org\/ru\/wp-json\/wp\/v2\/comments?post=395"}],"version-history":[{"count":0,"href":"https:\/\/colliot.org\/ru\/wp-json\/wp\/v2\/posts\/395\/revisions"}],"wp:attachment":[{"href":"https:\/\/colliot.org\/ru\/wp-json\/wp\/v2\/media?parent=395"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/colliot.org\/ru\/wp-json\/wp\/v2\/categories?post=395"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/colliot.org\/ru\/wp-json\/wp\/v2\/tags?post=395"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}