GSoC 2019: Gwirio graffiau am drawsnewidyddion dwyranoldeb a monad

Yr haf diwethaf cymerais ran ynddo Google Haf y Cod - rhaglen i fyfyrwyr o Google. Bob blwyddyn, mae'r trefnwyr yn dewis sawl prosiect Ffynhonnell Agored, gan gynnwys o blith sefydliadau adnabyddus fel Boost.org и Sefydliad Linux. Mae Google yn gwahodd myfyrwyr o bob rhan o'r byd i weithio ar y prosiectau hyn. 

Fel cyfranogwr yn Google Summer of Code 2019, fe wnes i brosiect yn y llyfrgell alga gyda'r sefydliad Haskell.org, sy'n datblygu iaith Haskell - un o'r ieithoedd rhaglennu swyddogaethol enwocaf. Mae Alga yn llyfrgell sy'n cynrychioli math yn ddiogel cynrychiolaeth ar gyfer graffiau yn Haskell. Fe'i defnyddir, er enghraifft, yn semantig — llyfrgell Github sy'n adeiladu coed semantig, graffiau galwadau a dibyniaeth yn seiliedig ar god ac sy'n gallu eu cymharu. Fy mhrosiect oedd ychwanegu cynrychiolaeth math-ddiogel ar gyfer graffiau deuran ac algorithmau ar gyfer y gynrychiolaeth honno. 

Yn y swydd hon byddaf yn siarad am fy ngweithrediad o algorithm ar gyfer gwirio graff ar gyfer dwyranoldeb yn Haskell. Er bod yr algorithm yn un o'r rhai mwyaf sylfaenol, fe gymerodd sawl iteriad i mi ei weithredu'n hyfryd mewn arddull swyddogaethol ac roedd angen cryn dipyn o waith. O ganlyniad, penderfynais ar weithrediad gyda thrawsnewidwyr monad. 

GSoC 2019: Gwirio graffiau am drawsnewidyddion dwyranoldeb a monad

Amdanaf fy hun

Fy enw i yw Vasily Alferov, rwy'n fyfyriwr yn y bedwaredd flwyddyn yn St. Petersburg HSE. Yn gynharach yn y blog ysgrifennais am fy mhrosiect am algorithmau paramedr и am y daith i ZuriHac. Ar hyn o bryd rydw i ar interniaeth yn Prifysgol Bergen yn Norwy, lle’r wyf yn gweithio ar ddulliau o fynd i’r afael â’r broblem Lliwio Rhestr. Mae fy niddordebau yn cynnwys algorithmau paramedr a rhaglennu swyddogaethol.

Ynglŷn â gweithredu'r algorithm

Rhagair

Anogir myfyrwyr sy'n cymryd rhan yn y rhaglen yn gryf i flogio. Fe wnaethon nhw roi llwyfan i mi ar gyfer y blog Haf Haskell. Mae'r erthygl hon yn gyfieithiad erthyglau, a ysgrifenwyd gennyf yno yn Gorphenaf yn Saesonaeg, gyda rhagymadrodd byr. 

Gellir dod o hyd i Cais Tynnu gyda'r cod dan sylw yma.

Gallwch ddarllen am ganlyniadau fy ngwaith (yn Saesneg) yma.

Bwriad y swydd hon yw ymgyfarwyddo'r darllenydd â'r cysyniadau sylfaenol mewn rhaglennu swyddogaethol, er y byddaf yn ceisio dwyn i gof yr holl dermau a ddefnyddir pan ddaw'r amser.

Gwirio graffiau am ddwyranoldeb 

Mae algorithm ar gyfer gwirio graff am ddwyranoldeb fel arfer yn cael ei roi mewn cwrs ar algorithmau fel un o'r algorithmau graff symlaf. Mae ei syniad yn syml: yn gyntaf rydym rywsut yn rhoi fertigau yn y gyfran chwith neu dde, a phan ganfyddir ymyl sy'n gwrthdaro, rydym yn haeru nad yw'r graff yn ddeuran.

Ychydig mwy o fanylion: yn gyntaf rydyn ni'n rhoi rhywfaint o fertig yn y gyfran chwith. Yn amlwg, rhaid i holl gymdogion y fertig hwn orwedd yn y llabed dde. Ymhellach, rhaid i holl gymdogion cymdogion y fertig hwn orwedd yn y llabed chwith, ac yn y blaen. Rydym yn parhau i aseinio cyfranddaliadau i fertigau cyn belled â bod fertigau o hyd yn y gydran gysylltiedig o'r fertig y gwnaethom ddechrau ag ef nad ydym wedi neilltuo cymdogion iddynt. Yna byddwn yn ailadrodd y weithred hon ar gyfer yr holl gydrannau cysylltiedig.

Os oes ymyl rhwng fertigau sy'n disgyn i'r un rhaniad, nid yw'n anodd dod o hyd i gylchred odrif yn y graff, sy'n hysbys yn eang (ac yn eithaf amlwg) yn amhosibl mewn graff deuran. Fel arall, mae gennym raniad cywir, sy'n golygu bod y graff yn ddeuran.

Yn nodweddiadol, mae'r algorithm hwn yn cael ei weithredu gan ddefnyddio ehangder chwiliad cyntaf neu chwiliad cyntaf dyfnder. Mewn ieithoedd gorchmynnol, defnyddir chwiliad manwl-gyntaf fel arfer gan ei fod ychydig yn symlach ac nid oes angen strwythurau data ychwanegol. Dewisais hefyd chwiliad dyfnder-gyntaf gan ei fod yn fwy traddodiadol.

Felly, daethom at y cynllun canlynol. Rydyn ni'n croesi fertigau'r graff gan ddefnyddio chwiliad manwl yn gyntaf ac yn aseinio cyfrannau iddyn nhw, gan newid rhif y gyfran wrth i ni symud ar hyd yr ymyl. Os byddwn yn ceisio aseinio cyfran i fertig sydd eisoes â chyfran wedi'i neilltuo, gallwn ddweud yn ddiogel nad yw'r graff yn ddeuran. Yr eiliad y rhoddir cyfran i bob fertig ac rydym wedi edrych ar yr ymylon i gyd, mae gennym raniad da.

Purdeb cyfrifiadau

Yn Haskell tybiwn fod yr holl gyfrifiadau glan. Fodd bynnag, pe bai hyn yn wir, ni fyddai gennym unrhyw ffordd i argraffu unrhyw beth i'r sgrin. O gwbl, yn lân mae cyfrifiadau mor ddiog fel nad oes un yn lân rhesymau dros gyfrifo rhywbeth. Mae'r holl gyfrifiadau sy'n digwydd yn y rhaglen yn cael eu gorfodi i mewn rhywsut "aflan" monad IO.

Mae Monas yn ffordd o gynrychioli cyfrifiadau gyda effeithiau yn Haskell. Mae esbonio sut maen nhw'n gweithio y tu hwnt i gwmpas y swydd hon. Gellir darllen disgrifiad da a chlir yn Saesneg yma.

Yma rwyf am nodi, er bod rhai monads, fel IO, yn cael eu gweithredu trwy hud casglwr, mae bron pob un arall yn cael ei weithredu mewn meddalwedd ac mae'r holl gyfrifiadau ynddynt yn bur.

Mae yna lawer o effeithiau ac mae gan bob un ei monad ei hun. Mae hon yn ddamcaniaeth gref a hardd iawn: mae pob monad yn gweithredu'r un rhyngwyneb. Byddwn yn siarad am y tri monad canlynol:

  • Naill ai mae ea yn gyfrifiad sy'n dychwelyd gwerth math a neu'n taflu eithriad o fath e. Mae ymddygiad y monad hwn yn debyg iawn i drin eithriadau mewn ieithoedd gorchmynnol: gellir dal neu drosglwyddo gwallau. Y prif wahaniaeth yw bod y monad yn cael ei weithredu'n gwbl resymegol yn y llyfrgell safonol yn Haskell, tra bod ieithoedd gorchmynnol fel arfer yn defnyddio mecanweithiau system weithredu.
  • Mae State sa yn gyfrifiad sy'n dychwelyd gwerth math a ac sydd â mynediad at gyflwr mudol math s.
  • Efallai a. Mae'r monad Maybe yn mynegi cyfrifiant y gellir ymyrryd ag ef ar unrhyw adeg trwy ddychwelyd Dim byd. Fodd bynnag, byddwn yn siarad am weithrediad y dosbarth MonadPlus ar gyfer y math Efallai, sy'n mynegi'r effaith groes: mae'n gyfrifiad y gellir ei dorri ar unrhyw adeg trwy ddychwelyd gwerth penodol.

Gweithredu'r algorithm

Mae gennym ddau fath o ddata, Graff a a Bigraff ab, y mae'r cyntaf ohonynt yn cynrychioli graffiau â fertigau wedi'u labelu â gwerthoedd math a, a'r ail yn cynrychioli graffiau deuran gyda fertigau ochr chwith wedi'u labelu â gwerthoedd math a a de -fertigau ochr wedi'u labelu â gwerthoedd math b.

Nid yw'r rhain yn fathau o lyfrgell Alga. Nid oes gan Alga gynrychiolaeth ar gyfer graffiau deuran angyfeiriedig. Gwneuthum y mathau fel hyn er eglurder.

Bydd angen swyddogaethau cynorthwyydd arnom hefyd gyda'r llofnodion canlynol:

-- Список соседей данной вершины.
neighbours :: Ord a => a -> Graph a -> [a]

-- Построить двудольный граф по графу и функции, для каждой вершины
-- выдающей её долю и пометку в новой доле, игнорируя конфликтные рёбра.
toBipartiteWith :: (Ord a, Ord b, Ord c) => (a -> Either b c)
                                         -> Graph a
                                         -> Bigraph b c

-- Список вершин в графе
vertexList :: Ord a => Graph a -> [a]
Сигнатура функции, которую мы будем писать, выглядит так:

type OddCycle a = [a]
detectParts :: Ord a => Graph a -> Either (OddCycle a) (Bigraph a a)

Mae'n hawdd gweld, os byddwn yn dod o hyd i ymyl sy'n gwrthdaro yn ystod y chwiliad dyfnder cyntaf, mae'r cylchred rhyfedd yn gorwedd ar ben y pentwr dychwelyd. Felly, i'w adfer, mae angen i ni dorri popeth o'r pentwr dychweliad hyd at ddigwyddiad cyntaf y fertig olaf.

Rydym yn gweithredu chwiliad manwl yn gyntaf trwy gynnal amrywiaeth cysylltiadol o rifau cyfrannau ar gyfer pob fertig. Bydd y pentwr dychweliad yn cael ei gynnal yn awtomatig trwy weithredu dosbarth Functor y monad yr ydym wedi'i ddewis: dim ond yr holl fertigau o'r llwybr y bydd angen i ni eu rhoi yn y canlyniad a ddychwelwyd o'r swyddogaeth ailadroddus.

Fy syniad cyntaf oedd defnyddio'r monad Naill ai, sy'n ymddangos fel pe bai'n gweithredu'r union effeithiau sydd eu hangen arnom. Roedd y gweithrediad cyntaf a ysgrifennais yn agos iawn at yr opsiwn hwn. Yn wir, cefais bum gweithrediad gwahanol ar un adeg ac yn y pen draw setlo ar un arall.

Yn gyntaf, mae angen i ni gynnal amrywiaeth cysylltiadol o ddynodwyr cyfrannau - mae hyn yn rhywbeth am y Wladwriaeth. Yn ail, mae angen inni allu stopio pan ganfyddir gwrthdaro. Gall hyn fod naill ai Monad ar gyfer Naill ai, neu MonadPlus ar gyfer Efallai. Y prif wahaniaeth yw y gall Naill ai ddychwelyd gwerth os nad yw'r cyfrifiad wedi'i atal, ac efallai y bydd yn dychwelyd gwybodaeth am hyn yn yr achos hwn yn unig. Gan nad oes angen gwerth ar wahân ar gyfer llwyddiant (mae eisoes wedi'i storio yn y Wladwriaeth), rydym yn dewis Efallai. Ac ar hyn o bryd pan fydd angen i ni gyfuno effeithiau dau monad, maen nhw'n dod allan trawsnewidyddion monad, sy'n cyfuno'r effeithiau hyn yn union.

Pam dewisais fath mor gymhleth? Dau reswm. Yn gyntaf, mae'r gweithredu yn debyg iawn i'r rheidrwydd. Yn ail, mae angen inni drin y gwerth dychwelyd rhag ofn y bydd gwrthdaro wrth ddychwelyd yn ôl o recursion i adfer y ddolen od, sy'n llawer haws i'w wneud yn y Efallai monad.

Felly cawn y gweithrediad hwn.

{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE ScopedTypeVariables #-}

data Part = LeftPart | RightPart

otherPart :: Part -> Part
otherPart LeftPart  = RightPart
otherPart RightPart = LeftPart

type PartMap a = Map.Map a Part
type OddCycle a = [a]

toEither :: Ord a => PartMap a -> a -> Either a a
toEither m v = case fromJust (v `Map.lookup` m) of
                    LeftPart  -> Left  v
                    RightPart -> Right v

type PartMonad a = MaybeT (State (PartMap a)) [a]

detectParts :: forall a. Ord a => Graph a -> Either (OddCycle a) (Bigraph a a)
detectParts g = case runState (runMaybeT dfs) Map.empty of
                     (Just c, _)  -> Left  $ oddCycle c
                     (Nothing, m) -> Right $ toBipartiteWith (toEither m) g
    where
        inVertex :: Part -> a -> PartMonad a
        inVertex p v = ((:) v) <$> do modify $ Map.insert v p
                                      let q = otherPart p
                                      msum [ onEdge q u | u <- neigbours v g ]

        {-# INLINE onEdge #-}
        onEdge :: Part -> a -> PartMonad a
        onEdge p v = do m <- get
                        case v `Map.lookup` m of
                             Nothing -> inVertex p v
                             Just q  -> do guard (q /= p)
                                           return [v]

        processVertex :: a -> PartMonad a
        processVertex v = do m <- get
                             guard (v `Map.notMember` m)
                             inVertex LeftPart v

        dfs :: PartMonad a
        dfs = msum [ processVertex v | v <- vertexList g ]

        oddCycle :: [a] -> [a]
        oddCycle c = tail (dropWhile ((/=) last c) c)

Y bloc lle yw craidd yr algorithm. Byddaf yn ceisio egluro beth sy'n digwydd y tu mewn iddo.

  • inVertex yw'r rhan o chwiliad manwl-gyntaf lle rydym yn ymweld â'r fertig am y tro cyntaf. Yma rydym yn neilltuo rhif cyfranddaliad i'r fertig ac yn rhedeg onEdge ar bob cymydog. Dyma hefyd lle rydym yn adfer y pentwr galwadau: pe bai msum yn dychwelyd gwerth, rydym yn gwthio fertex v yno.
  • OnEdge yw'r rhan lle rydyn ni'n ymweld â'r ymyl. Fe'i gelwir ddwywaith ar gyfer pob ymyl. Yma rydym yn gwirio a ymwelwyd â'r fertig ar yr ochr arall, ac yn ymweld ag ef os na. Os ymwelir â hi, byddwn yn gwirio a yw'r ymyl yn gwrthdaro. Os ydyw, byddwn yn dychwelyd y gwerth - pen uchaf y pentwr dychweliad, lle bydd yr holl fertigau eraill yn cael eu gosod ar ôl eu dychwelyd.
  • processVertex yn gwirio ar gyfer pob fertig a ymwelwyd ag ef ac yn rhedeg inVertex arno os na.
  • Mae dfs yn rhedeg processVertex ar bob fertig.

Dyna i gyd.

Hanes y gair INLINE

Nid oedd y gair INLINE yng ngweithrediad cyntaf yr algorithm; ymddangosodd yn ddiweddarach. Pan geisiais ddod o hyd i weithrediad gwell, canfûm fod y fersiwn nad yw'n INLINE yn amlwg yn arafach ar rai graffiau. O ystyried y dylai'r swyddogaethau weithio'r un peth yn semantig, roedd hyn wedi fy synnu'n fawr. Hyd yn oed dieithryn, ar beiriant arall gyda fersiwn gwahanol o GHC nid oedd gwahaniaeth amlwg.

Ar ôl treulio wythnos yn darllen allbwn Craidd GHC, llwyddais i drwsio'r broblem gydag un llinell o INLINE eglur. Ar ryw adeg rhwng GHC 8.4.4 a GHC 8.6.5 rhoddodd y optimizer y gorau i wneud hyn ar ei ben ei hun.

Nid oeddwn yn disgwyl dod ar draws baw o'r fath mewn rhaglennu Haskell. Fodd bynnag, hyd yn oed heddiw, mae optimizers weithiau'n gwneud camgymeriadau, a'n gwaith ni yw rhoi awgrymiadau iddynt. Er enghraifft, yma rydym yn gwybod y dylai'r ffwythiant gael ei leinio oherwydd ei fod wedi'i leinio yn y fersiwn hanfodol, ac mae hyn yn rheswm i roi awgrym i'r casglwr.

Beth ddigwyddodd nesaf?

Yna gweithredais algorithm Hopcroft-Karp gyda monads eraill, a dyna oedd diwedd y rhaglen.

Diolch i Google Summer of Code, cefais brofiad ymarferol mewn rhaglennu swyddogaethol, a oedd nid yn unig wedi fy helpu i gael interniaeth yn Jane Street yr haf canlynol (nid wyf yn siŵr pa mor adnabyddus yw'r lle hwn hyd yn oed ymhlith cynulleidfa wybodus Habr, ond mae'n un o'r ychydig lle gallwch chi haf i gymryd rhan mewn rhaglennu swyddogaethol), ond hefyd wedi fy nghyflwyno i'r byd gwych o gymhwyso'r patrwm hwn yn ymarferol, sy'n sylweddol wahanol i fy mhrofiad mewn ieithoedd traddodiadol.

Ffynhonnell: hab.com

Ychwanegu sylw