Najmniej ścisłe (*)

Question

Czy możliwe jest zaimplementowanie (*) z najmniej ścisłą semantyką w Haskell (preferowana jest standardowa Haskell, ale rozszerzenia są w porządku, czy używanie wewnętrznych kompilacji jest oszustwem)? Na przykład, taka definicja powinna spowodować następujące jest prawdziwe:

0 * ⊥ = 0 
⊥ * 0 = 0 

i wyłącznie:

⊥ * ⊥ = ⊥ 

mogę zbudować wzorzec pasuje, które spełniają jeden z powyższych przypadków, ale nie jednocześnie, ponieważ kontrola zerowa wymusza wartość.

Answer 1

Tak, ale tylko przy użyciu ograniczonego zanieczyszczenia.

laziestMult :: Num a => a -> a -> a 
laziestMult a b = (a * b) `unamb` (b * a) 

tutaj unamb jest "czysta" wariant Conal Elliotta z amb. Operacyjnie, dwie równoległe obliczenia, które powracają, stają się pierwsze. Denotacyjnie unamb przyjmuje dwie wartości, gdzie jedna jest ściśle większa (w rozumieniu teorii domeny) niż druga, i zwraca większą. Edytuj: również to jest unamb, nie lub, więc musisz mieć je równe, chyba że jeden jest na dole. W związku z tym istnieje wymóg semantyczny, który musi obowiązywać, mimo że nie może być wymuszony przez system typów. Jest to realizowane zasadniczo:

unamb a b = unsafePerformIO $ amb a b 

wiele pracy polega na tym, aby wszystko działało poprawnie z wyjątkami/zarządzaniem zasobami/bezpieczeństwem wątków.

laziestMult jest poprawny, jeśli * jest przemienny. Jest "najmniej rygorystyczne", jeśli * nie jest ścisłe w jednym argumencie.

uzyskać więcej informacji, zobacz odpowiedź Conal's blog

Answer 2

Phillip JF dotyczy tylko domen płaskie, ale istnieją Num przypadki, które nie są płaskie, na przykład leniwe kasowniki. Kiedy wchodzisz na tę arenę, sprawy stają się subtelne.

data Nat = Zero | Succ Nat 
    deriving (Show) 

instance Num Nat where 
    x + Zero = x 
    x + Succ y = Succ (x + y) 

    x * Zero = Zero 
    x * Succ y = x + x * y 

    fromInteger 0 = Zero 
    fromInteger n = Succ (fromInteger (n-1)) 

    -- we won't need the other definitions 

Jest szczególnie ważne dla leniwych naturali, że operacje są najmniej surowe, ponieważ jest to domena ich użycia; na przykład używamy ich do porównywania długości potencjalnie nieskończonych list, a jeśli jego operacje nie są najmniej ścisłe, to rozbieżność będzie się wiązać z uzyskaniem użytecznych informacji.

Zgodnie z oczekiwaniami, (+) nie jest przemienne:

ghci> undefined + Succ undefined 
Succ *** Exception: Prelude.undefined 
ghci> Succ undefined + undefined 
*** Exception: Prelude.undefined 

Więc będziemy stosować standardowe sztuczki, aby to zrobić:

laxPlus :: Nat -> Nat -> Nat 
laxPlus a b = (a + b) `unamb` (b + a) 

który wydaje się działać na pierwszy

ghci> undefined `laxPlus` Succ undefined 
Succ *** Exception: Prelude.undefined 
ghci> Succ undefined `laxPlus` undefined 
Succ *** Exception: Prelude.undefined 

, ale w rzeczywistości nie jest to

ghci> Succ (Succ undefined) `laxPlus` Succ undefined 
Succ (Succ *** Exception: Prelude.undefined 
ghci> Succ undefined `laxPlus` Succ (Succ undefined) 
Succ *** Exception: Prelude.undefined 

Dzieje się tak, ponieważ Nat nie jest domeną płaską, a unamb dotyczy tylko domen płaskich.Z tego powodu uważam, że unamb jest prymitywem niskiego poziomu, którego nie powinno się używać, z wyjątkiem definiowania koncepcji wyższego poziomu - nie powinno mieć znaczenia, czy domena jest płaska. Używanie unamb będzie czułe na czynniki, które zmieniają strukturę domeny - ten sam powód jest bardzo brzydki. Musimy uogólnić unamb w ten sam sposób, w jaki seq jest uogólnione na deeqSeq: odbywa się to w module Data.Lub. Musimy najpierw napisać instancji HasLub dla Nat:

instance HasLub Nat where 
    lub a b = unambs [ 
        case a of 
         Zero -> Zero 
         Succ _ -> Succ (pa `lub` pb), 
        case b of 
         Zero -> Zero 
         Succ _ -> Succ (pa `lub` pb) 
       ] 
     where 
     Succ pa = a 
     Succ pb = b 

Zakładając, to jest prawdziwe, co niekoniecznie jest przypadek (nie jest to mój trzeci spróbować tej pory), możemy teraz napisać laxPlus':

laxPlus' :: Nat -> Nat -> Nat 
laxPlus' a b = (a + b) `lub` (b + a) 

i to rzeczywiście działa:

ghci> Succ undefined `laxPlus'` Succ (Succ undefined) 
Succ (Succ *** Exception: Prelude.undefined 
ghci> Succ (Succ undefined) `laxPlus'` Succ undefined 
Succ (Succ *** Exception: Prelude.undefined 

Więc są napędzane uogólniać, że najsłabiej ścisłym wzorcem dla przemiennej operatora binarnego s to:

leastStrict :: (HasLub a) => (a -> a -> a) -> a -> a -> a 
leastStrict f x y = f x y `lub` f y x 

Przynajmniej gwarantuje się przemianę. Ale, niestety, istnieją dalsze problemy:

ghci> Succ (Succ undefined) `laxPlus'` Succ (Succ undefined) 
Succ (Succ *** Exception: BothBottom 

Oczekujemy sumę dwóch liczb, które są co najmniej 2 musi wynosić co najmniej 4, ale tu mamy pewną liczbę, która jest tylko co najmniej 2. Nie mogę przyjść ze sposobem modyfikacji leastStrict, aby dać nam pożądany wynik, przynajmniej nie bez wprowadzenia nowego ograniczenia klasy. Aby rozwiązać ten problem, musimy kopać w rekurencyjnej definicji, a jednocześnie wzór mecz na obu argumentów na każdym kroku:

laxPlus'' :: Nat -> Nat -> Nat 
laxPlus'' a b = lubs [ 
    case a of 
     Zero -> b 
     Succ a' -> Succ (a' `laxPlus''` b), 
    case b of 
     Zero -> a 
     Succ b' -> Succ (a `laxPlus''` b') 
    ] 

I wreszcie mamy taki, który daje tak wiele informacji, jak to możliwe, wierzę:

ghci> Succ (Succ undefined) `laxPlus''` Succ (Succ undefined) 
Succ (Succ (Succ (Succ *** Exception: BothBottom 

Jeśli zastosujemy ten sam wzór do czasów, mamy coś, co wydaje się działać także:

laxMult :: Nat -> Nat -> Nat 
laxMult a b = lubs [ 
    case a of 
     Zero -> Zero 
     Succ a' -> b `laxPlus''` (a' `laxMult` b), 
    case b of 
     Zero -> Zero 
     Succ b' -> a `laxPlus''` (a `laxMult` b') 
    ] 

ghci> Succ (Succ undefined) `laxMult` Succ (Succ (Succ undefined)) 
Succ (Succ (Succ (Succ (Succ (Succ *** Exception: BothBottom 

Nie trzeba dodawać, że jest tu kilka powtarzających się kodów, a rozwijanie schematów w celu wyrażenia tych funkcji w sposób zwięzły (a zatem z jak najmniejszymi możliwościami błędu) byłoby interesującym ćwiczeniem. Mamy jednak inny problem ...

asLeast :: Nat -> Nat 
atLeast Zero = undefined 
atLeast (Succ n) = Succ (atLeast n) 

ghci> atLeast 7 `laxMult` atLeast 7 
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ ^CInterrupted. 

Jest strasznie powolny. Jest tak oczywiście dlatego, że jest (przynajmniej) wykładniczy w rozmiarze swoich argumentów, zstępując na dwie gałęzie każdej rekursji. Będzie wymagać jeszcze większej subtelności, aby uruchomić go w rozsądnym czasie.

Najmniej rygorystyczne programowanie jest stosunkowo nieodkrytym terytorium i istnieje potrzeba dalszych badań, zarówno w zakresie wdrażania, jak i praktycznych zastosowań. Jestem podekscytowany i uważam to za obiecujące terytorium.