Abstraktní Wikipedie/Aktualizace/2022-04-01

This page is a translated version of the page Abstract Wikipedia/Updates/2022-04-01 and the translation is 100% complete.
Aktualizace Abstraktní Wikipedie Translate

Abstraktní Wikipedie prostřednictvím e-mailového seznamu Abstraktní Wikipedie na IRC Wikifunkce na Telegramu Wikifunkce na Facebooku Wikifunkce na Twitteru Wikifunkce na Facebooku Wikifunkce na YouTube Webové stránky Wikifunkcí Translate

Typované seznamy jsou dloooouhé

Dnešní newsletter se zaměří na technický detail a pokud se nechcete ponořit do detailů našeho datového modelu, klidně jej přeskočte.

V posledních několika týdnech jsme opakovaně narazili na překážku, kterou se nám zatím nepodařilo vyřešit, a to jak reprezentovat typovaný seznam, aniž by se reprezentace stala velmi dlouhou. Seznam ve Wikifunkcích je typ, který obsahuje neznámý počet prvků v určitém pořadí.

V datovém modelu Wikifunkcí je seznam reprezentován stejným způsobem jako v programovacím jazyce Lisp: seznam se skládá ze dvou částí, "hlavy" (head), což je první prvek seznamu, a "ocasu" (tail), který je sám seznamem a obsahuje zbytek seznamu. Kromě toho existuje prázdný seznam, který nemá žádnou hlavu ani ocas a představuje seznam s nulovými prvky. Ve Wikifunkcích je typem pro seznam Z10/List (Seznam).

Takže seznam o dvou prvcích "a" a "b" by, v naší JSON notaci, vypadal takto:

{
  "type": "Seznam",
  "head": "a"
  "tail": {
    "type": "Seznam",
    "head": "b",
    "tail": {
      "type": "Seznam"
    }
  }
}
{
  "Z1K1": "Z10",
  "Z10K1": "a"
  "Z10K2": {
    "Z1K1": "Z10",
    "Z10K1": "b",
    "Z10K2": {
      "Z1K1": "Z10"
    }
  }
}

Protože je to trochu dlouhé, zavedli jsme zkratku pomocí zápisu pole v JSONu, takže seznam lze reprezentovat takto:

[ "a", "b" ]

Krátký zápis (říkáme mu kanonizovaný) lze snadno a mechanicky převést na delší zápis, který vidíme výše, a naopak.

Ve fázi η jsme zavedli možnost typovaných seznamů. Zatímco v normálním seznamu neříkáme nic o typu prvků seznamu, v typovaném seznamu říkáme "každý prvek seznamu musí být určitého typu". Mít typované seznamy nám umožňuje mít silnější záruky k typování: pokud se zeptáte na prvek typovaného seznamu, víte, jakého typu bude výsledek. To může být užitečné při kontrole typů a při poskytování lepších rozhraní.

Typovaný seznam je výsledkem volání funkce. Máme funkci Z881/Typed list (Typovaný seznam), která jako jediný argument přijímá type (typ) a vrací type (typ). Výsledný type (typ) je kopií typu Z10/List (Seznam) s tím rozdílem, že místo aby hlava (head) měla hodnotu libovolného typu, musí mít hodnotu typu zadaného jako argument. A ocas (tail) není typu Z10/List (Seznam), ale typu vráceného voláním Z881/Type list (Typovaný seznam) s daným typem argumentu.

Řekněme, že chceme reprezentovat seznam, který jsme měli předtím, ale místo toho, aby to byl Z10/List (Seznam), měl by to být seznam řetězců. Seznam řetězců je typ, který vytvoříme voláním funkce Z881/Typed list (Typovaný seznam) na typu Z6/String (Řetězec). V notaci JSON by to vypadalo následovně.

{
  "type": {
    "type": "Function call (Volání funkce)",
    "function": "Typed list (Typovaný seznam)",
    "argument type": "String (Řetězec)"
  },
  "head": "a"
  "tail": {
    "type": {
      "type": "Function call (Volání funkce)",
      "function": "Typed list (Typovaný seznam)",
      "argument type": "String (Řetězec)"
    },
    "head": "b",
    "tail": {
      "type": {
        "type": "Function call (Volání funkce)",
        "function": "Typed list (Typovaný seznam)",
        "argument type": "String (Řetězec)"
      }
    }
  }
}
{
  "Z1K1": {
    "Z1K1": "Z7",
    "Z7K1": "Z881",
    "Z881K1": "Z6"
  },
  "K1": "a"
  "K2": {
    "Z1K1": {
      "Z1K1": "Z7",
      "Z7K1": "Z881",
      "Z881K1": "Z6"
    },
    "Z10K1": "b",
    "Z10K2": {
      "Z1K1": {
        "Z1K1": "Z7",
        "Z7K1": "Z881",
        "Z881K1": "Z6"
      }
    }
  }
}

Problém je v tom, že pro to nemůžeme mít stejný krátký zápis, protože bychom ztratili informace.

Pokusili jsme se to obejít odhadem typu: podíváme se do seznamu, a pokud má vše stejný typ, prohlásíme jej za typovaný seznam. Ale jednak to kód docela komplikuje a jednak to stále neřeší všechny problémy: zkrácená podoba výše uvedeného seznamu může být skutečně seznamem objektů, nebo to může být seznam řetězců - nemáme možnost to zjistit.

Nyní zveřejňujeme naši interní diskusi a několik možností a rádi bychom si vyslechli vaše názory a získali širší podněty.