Upgrade to Pro — share decks privately, control downloads, hide ads and more …

switchのexhaustiveness/redundancy チェック 理論と実装 わいわ...

ukitaka
December 31, 2019

switchのexhaustiveness/redundancy チェック 理論と実装 わいわいswiftc #8 @ukitaka

swiftcがいかにしてswitchの網羅性チェックをしているかを、背景にあるSpaceという概念を元にしたパターンマッチの網羅性チェックの理論とその実装について、lib/Sema/TypeCheckSwitchStmt.cppとソースコード中で紹介されている論文を元に紹介します。

ukitaka

December 31, 2019
Tweet

More Decks by ukitaka

Other Decks in Programming

Transcript

  1. Space EngineΛ༻͍ͨ໢ཏੑνΣοΫ ࢀߟจݙ ▸ Maranget, Luc. "Warnings for pattern matching."

    Journal of Functional Programming 17.3 (2007): 387-421. ▸ ͜Ε͕ԼͷPaperͷϕʔεͱͳͬͨ࿦จ ▸ (GenericͰͳ͍) ୅਺తσʔλܕΛѻ͑ΔܕγεςϜʹ͓͚Δ໢ཏੑνΣοΫͷΞϧΰϦζϜ ▸ A generic algorithm for checking exhaustivity of pattern matching, F. Liu, Scala 16’, 2017 ▸ ͕ͬͪ͜SpaceΛ࢖ͬͨ໢ཏੑݕࠪʹؔ͢Δ࿦จɺ͜ΕΛԠ༻ͯ͠৑௕ੑݕࠪ΋ߦ͏ ▸ ಛఆͷܕγεςϜʹґଘ͠ͳ͍ΞϧΰϦζϜ ( GADTs΋ѻ͑Δ )
  2. Space EngineΛ༻͍ͨ໢ཏੑνΣοΫ A Generic Algorithm for Checking Exhaustivity of Pattern

    Matching ▸ ݩʑ͸Dottyͱ͍͏ScalaͷίϯύΠϥ (Scala 3.0~)Ͱ࠾༻͞Ε͍ͯΔ΋ͷΛSwift ʹҠ২͖ͯͨ͠΋ͷɻ https://fengy.me/
  3. Space EngineΛ༻͍ͨ໢ཏੑνΣοΫ A Generic Algorithm for Checking Exhaustivity of Pattern

    Matching ▸ ໢ཏੑνΣοΫͷΞϧΰϦζϜΛಛఆͷܕγεςϜ͔Β੾Γ཭͠ɺͲͷΑ͏ͳݴ ޠ(ͷܕγεςϜ)Ͱ΋࢖͑ΔΑ͏ͳҰൠతͳΞϧΰϦζϜΛఏڙ͢Δ ▸ ྫͱͯ͠Scala (Dotty) ͷܕγεςϜ΁ͷԠ༻Λ͍ࣔͯ͠Δ ▸ ϑΥʔϚϧͳূ໌͕͋ΔΘ͚Ͱ͸ͳ͍͚Ͳɺ͋Δఔ౓ෳࡶͳܕγεςϜΛ΋ͭ ScalaͰͷ࠾༻࣮੷͕͋Δ ▸ ͪͳΈʹFengyun Liuࢯͷࢦಋڭһ͸Oderskyઌੜ
  4. Space EngineΛ༻͍ͨ໢ཏੑνΣοΫ ͦ΋ͦ΋SpaceҎલͷ࣮૷ ▸ ݕࠪ͢Δର৅ͷܕ (Subject type) ͔Β֤έʔεΛ औΓআ͍ͯߦͬͯ࢒Γ͕ͳ͍͔ݟΔɺΈ͍ͨͳ࣮ ૷

    ▸ ࣮͸SpaceΛ༻͍࣮ͨ૷ʹ͍ۙ͜ͱΛ͍ͯ͠Δ ͕ɺ͍͔ͭ͘໰୊͕͋ͬͨͨΊScala (Dotty)Ͱͷ ࣮੷ͷ͋ΔํࣜΛվΊͯ࠾༻
  5. SpaceΛ༻͍ͨ”໢ཏ”ͷఆࣜԽ Space Engineͷ࣮૷ΛಡΉʹ͋ͨͬͯ ▸ SwiftͰͷ໢ཏੑνΣοΫͷ࣮૷Λཧղ͢ΔͨΊʹΞϧΰϦζϜΛ஌Δඞཁ͕͋Δ ▸ ΞϧΰϦζϜΛཧղ͢ΔͨΊʹ͸ Spaceʹؔ͢Δ༻ޠ΍ͦͷఆٛΛཧղ͓ͯ͘͠ ඞཁ͕͋Δ ▸

    SpaceʹΑͬͯఆࣜԽ͞Εͨ “໢ཏ͍ͯ͠Δ” ͜ͱΛද͍ͯ͠ΔࣜΛཧղ͢Δͷ͕ ࠷ॳͷ໨ඪ (T) ⪯ (p1 ) ∣ (p2 ) ∣ . . . ↑ ͜Ε͕໢ཏ͍ͯ͠Δ͜ͱΛදࣜ͢
  6. SpaceΛ༻͍ͨ”໢ཏ”ͷఆࣜԽ ఆٛ (Space) ▸ ܕ΍ύλʔϯ͕औΓ͏Δ஋ͷू߹ΛSpaceͱ͍͏ ▸ Space͸࠶ؼతʹҎԼͷΑ͏ʹఆٛ͞ΕΔ 1. ΛۭSpace (empty

    space) 2. ΛܕTͷSpace (type space) 3. ͕Spaceͷͱ͖ɺ Λ union space 4. ͕SpaceͰɺK͕Constructor Typeͷͱ͖ (T) s1 , s2 , . . . s1 |s2 | . . . s1 , s2 , . . . , sn (K, s1 , s2 , . . . , sn ) Λconstructor space
  7. Subspaceؔ܎ ఆٛ (Subspaceؔ܎) ▸ ΛSpace্ͷೋ߲ؔ܎ Subspaceؔ܎ ͱ͢Δ ⪯ s1 ⪯

    s2 ▸ ௚؍తʹ͸ू߹ͷแؚؔ܎͕ͩɺཁૉʹ͸௚઀ݴٴͤͣʹ ܕ΍ܕߏஙࢠ (case) ͷؔ܎Λ࢖ͬͯఆ͍ٛͯ͘͠ɻৄࡉͳϧʔϧ͸ޙड़ɻ
  8. Subspaceؔ܎ ఆٛ (projection) ▸ Λύλʔϯͱ͢Δɻ͜ͷͱ͖ ͕Χόʔ͢ΔSpaceΛ ͱද͢ ▸ ύλʔϯ =

    case ͱࢥͬͯࠩ͠ࢧ͑ͳ͍ (ਖ਼֬Ͱ͸ͳ͍) p (p) p ͬͪ͜͸type constructor ͬͪ͜͸pattern
  9. Subspaceؔ܎ ໢ཏͷఆࣜԽ (࠶ܝ) ▸ Ϛονͤ͞Δର৅ͷܕTʹ͍ͭͯɺ ͕͢΂ͯͷcase͕Χόʔ͍ͯ͠Δspace ͷunion spaceͷsubspaceʹͳ͍ͬͯΔ͔ ▸ ύλʔϯ

    ͕ ܕ TΛ໢ཏ͍ͯ͠Δͱ͸ҎԼΛຬͨ͢͜ͱͰ͋Δɻ (T) p1 , p2 , . . . (T) ⪯ (p1 ) ∣ (p2 ) ∣ . . . ͜͜·ͰͰ”໢ཏ”ͷ͕ࣜಡΊͨʂ(͸ͣʂ)
  10. Subspaceؔ܎ SpaceΛ༻͍ͨ”໢ཏ”ͷఆࣜԽ ▸ ໢ཏ͍ͯ͠Δ͜ͱΛSubspaceؔ܎Λ࢖ͬͯҎԼͷΑ͏ʹදͤͨ (T) ⪯ (p1 ) ∣ (p2

    ) ∣ . . . ▸ ࣍͸͜ͷSubspaceؔ܎ͷ۩ମతͳϧʔϧΛ·ͨผͷ֓೦Λ࢖ͬͯఆ͍ٛͯ͘͠…. (ΊΜͲ͍) s1 ⪯ s2 ⇔ s1 ⊖ s2 ≐ ΞϧΰϦζϜΛཧղ͢Δͷʹඞཁͳఆٛ͸ ͜ΕͰ࠷ޙͳͷͰ͕Μ͹Ζ͏…
  11. ▸ Subspaceؔ܎ΛSubtractionΛ༻͍ͯఆٛ͢Δ ▸ Space ʹ͍ͭͯɺ ͕ ҎԼΛຬͨ࣌͢(͔ͭͦͷ࣌ͷΈ) ͕ ͷ SubspaceͰ͋Δͱ͍͏

    ⊖Λ࢖ͬͨSubspaceؔ܎ͷఆٛ ఆٛ (Subspaceؔ܎) s1 , s2 s1 s2 s1 s2 s1 ⪯ s2 ⇔ s1 ⊖ s2 ≐
  12. ⊖Λ࢖ͬͨSubspaceؔ܎ͷఆٛ Subtractionͷϧʔϧ A generic algorithm for checking exhaustivity of pattern

    matching, F. Liu, Scala 16’, 2017 ΑΓҾ༻ empty spaceʹؔ͢Δϧʔϧ
  13. SpaceΛ༻͍ͨ”໢ཏ”ͷఆࣜԽ SpaceΛ༻͍ͨ”໢ཏ”ͷఆࣜԽ (T) ⪯ (p1 ) ∣ (p2 ) ∣

    . . . (T) ⊖ (p1 ) ∣ (p2 ) ∣ . . . ≐ “໢ཏ͍ͯ͠Δ” ͜͜·ͰΘ͔Ε͹ϝΠϯͷϩδοΫ͸ಡΊΔʂ
  14. Decompose Decompose ▸ enum E { case a, b }

    ͕͋ͬͨͱͯ͠ ͷܭࢉΛͲ͏ਐΊΔ ͔ʁ ▸ ͜ͷΑ͏ͳܭࢉΛਐΊΔͨΊʹܕEʹରͯ͠ Decompose (෼ղ) ͱ͍͏ૢ࡞Λఆ ٛ͢Δඞཁ͕͋Δ (E) ⊖ (a) ∣ (b)
  15. Decompose Decompose·ͰΘ͔Ε͹͍͍͍͚ͩͨΔ (E) ⊖ (a) ∣ (b) ≐ (E) ⪯

    (a) ∣ (b) ໢ཏ͍ͯ͠Δͱ͸ subtractionΛ࢖ͬͯ
  16. Decompose Decompose·ͰΘ͔Ε͹͍͍͍͚ͩͨΔ (E) ⊖ (a) ∣ (b) DecomposeΛ࢖ͬͯ (E) =

    (a) ∣ (b) (a) ∣ (b) ⊖ (a) ∣ (b) ͋ͱ͸Α͠ͳʹܭࢉΛਐΊΕ͹ (a) ∣ (b) ⊖ (a) ∣ (b) ≐
  17. ৑௕ੑνΣοΫ ৑௕ੑνΣοΫͷΞϧΰϦζϜ ▸ ໢ཏੑνΣοΫͷաఔͰ֤έʔεͷunion spaceΛܭࢉ͍ͯ͘͠ (T) ⪯ (p1 ) ∣

    (p2 ) ∣ . . . ͜ͷ෦෼ ▸ ܭࢉͷաఔͰɺ৽ͨʹ௥Ճ͢Δέʔε͕ͦ͜·Ͱͷunion spaceͷsubspaceʹ ͳ͍ͬͯͳ͍͔ΛνΣοΫ͢Δ (p1 ) ∣ (p2 )| . . . |(pn ) ⪯ (pn + 1)
  18. ৑௕ੑνΣοΫ ৑௕ੑνΣοΫͷΞϧΰϦζϜ (a) ∣ (b) ⪯ (c) (a) ∣ (b)

    ∣ (c) ⪯ (a) (a) ⪯ (b) ੒ཱ͠ͳ͍ͷͰOK ੒ཱ͢ΔͷͰ৑௕
  19. Where۟ Where۟ ▸ ܕ΍ܕߏஙࢠಉ࢜ͷؔ܎ʹج͍ͮͯSubspace(Subtraction)͕ఆٛ͞ΕΔ ▸ ஋ʹ௚઀ݴٴ͢ΔΑ͏ͳ΋ͷ͸͜ͷΞϧΰϦζϜͰ͸ѻ͑ͳ͍ ▸ 3.4 Limitations ʹ

    “Guards in pattern clauses pose a theoretical difficulty, thus are not handled by the algorithm.” ͱॻ͔Ε͍ͯΔ௨Γ
  20. Int