Błędna rozdzielczość typu otworu


105

Niedawno odkryłem, że dziury typu połączone z dopasowywaniem wzorców na próbach zapewniają całkiem przyjemne doświadczenie w stylu Agdy w Haskell. Na przykład:

{-# LANGUAGE
    DataKinds, PolyKinds, TypeFamilies, 
    UndecidableInstances, GADTs, TypeOperators #-}

data (==) :: k -> k -> * where
    Refl :: x == x

sym :: a == b -> b == a
sym Refl = Refl 

data Nat = Zero | Succ Nat

data SNat :: Nat -> * where
    SZero :: SNat Zero
    SSucc :: SNat n -> SNat (Succ n)

type family a + b where
    Zero   + b = b
    Succ a + b = Succ (a + b)

addAssoc :: SNat a -> SNat b -> SNat c -> (a + (b + c)) == ((a + b) + c)
addAssoc SZero b c = Refl
addAssoc (SSucc a) b c = case addAssoc a b c of Refl -> Refl

addComm :: SNat a -> SNat b -> (a + b) == (b + a)
addComm SZero SZero = Refl
addComm (SSucc a) SZero = case addComm a SZero of Refl -> Refl
addComm SZero (SSucc b) = case addComm SZero b of Refl -> Refl
addComm sa@(SSucc a) sb@(SSucc b) =
    case addComm a sb of
        Refl -> case addComm b sa of
            Refl -> case addComm a b of
                Refl -> Refl 

Naprawdę fajną rzeczą jest to, że mogę zastąpić prawe strony Refl -> expkonstrukcji otworem typu, a moje typy celów do otworów są aktualizowane o dowód, prawie tak jak w przypadku rewriteformularza w Agdzie.

Jednak czasami dziura po prostu nie aktualizuje się:

(+.) :: SNat a -> SNat b -> SNat (a + b)
SZero   +. b = b
SSucc a +. b = SSucc (a +. b)
infixl 5 +.

type family a * b where
    Zero   * b = Zero
    Succ a * b = b + (a * b)

(*.) :: SNat a -> SNat b -> SNat (a * b)
SZero   *. b = SZero
SSucc a *. b = b +. (a *. b)
infixl 6 *.

mulDistL :: SNat a -> SNat b -> SNat c -> (a * (b + c)) == ((a * b) + (a * c))
mulDistL SZero b c = Refl
mulDistL (SSucc a) b c = 
    case sym $ addAssoc b (a *. b) (c +. a *. c) of
        -- At this point the target type is
        -- ((b + c) + (n * (b + c))) == (b + ((n * b) + (c + (n * c))))
        -- The next step would be to update the RHS of the equivalence:
        Refl -> case addAssoc (a *. b) c (a *. c) of
            Refl -> _ -- but the type of this hole remains unchanged...

Ponadto, nawet jeśli typy docelowe niekoniecznie są wyrównane w dowodzie, jeśli wkleię całość z Agdy, nadal sprawdza się dobrze:

mulDistL' :: SNat a -> SNat b -> SNat c -> (a * (b + c)) == ((a * b) + (a * c))
mulDistL' SZero b c = Refl
mulDistL' (SSucc a) b c = case
    (sym $ addAssoc b (a *. b) (c +. a *. c),
    addAssoc (a *. b) c (a *. c),
    addComm (a *. b) c,
    sym $ addAssoc c (a *. b) (a *. c),
    addAssoc b c (a *. b +. a *. c),
    mulDistL' a b c
    ) of (Refl, Refl, Refl, Refl, Refl, Refl) -> Refl

Czy masz jakieś pomysły, dlaczego tak się dzieje (lub jak mogę zrobić poprawną korektę dowodu w solidny sposób)?


8
Nie spodziewasz się trochę dużo? Dopasowywanie wzorców w dowodzie równości polega na ustanowieniu (dwukierunkowej) równości. Nie jest wcale jasne, gdzie i w jakim kierunku chcesz go zastosować do typu celu. Na przykład możesz pominąć symwywołania, mulDistL'a kod nadal będzie sprawdzał.
kosmikus

1
Całkiem możliwe, że spodziewam się zbyt wiele. Jednak w wielu przypadkach działa tak samo, jak w Agdzie, więc nadal przydatne byłoby ustalenie prawidłowości zachowania. Nie jestem jednak optymistą, ponieważ sprawa jest prawdopodobnie głęboko związana z wnętrznościami weryfikatora typu.
András Kovács

1
Jest to trochę ortogonalne w stosunku do twojego pytania, ale możesz wyciągnąć te dowody, używając zestawu kombinatorów rozumowania równań à la Agda. Por. ten dowód koncepcji
gallais

Odpowiedzi:


1

Jeśli chcesz wygenerować wszystkie możliwe takie wartości, możesz napisać funkcję, która to zrobi, z podanymi lub określonymi granicami.

Może być całkiem możliwe użycie cyfr kościelnych na poziomie typu lub innych, aby wymusić ich tworzenie, ale jest to prawie zdecydowanie za dużo pracy, jak na to, czego prawdopodobnie chcesz / potrzebujesz.

To może nie być to, czego chcesz (np. „Z wyjątkiem używania tylko (x, y), ponieważ z = 5 - x - y”), ale ma to większy sens niż próba wprowadzenia pewnego rodzaju wymuszonego ograniczenia na poziomie typu, aby umożliwić prawidłowe wartości.


-3

Dzieje się tak, ponieważ wartości są określane w czasie wykonywania. Może spowodować transformację wartości w zależności od tego, co zostało wprowadzone w czasie wykonywania, dlatego zakłada, że ​​otwór jest już zaktualizowany.


3
Oczywiście wartości są określane w czasie wykonywania, ale nie ma to nic wspólnego z pytaniem. Niezbędne informacje są już dostępne z dopasowywania wzorców w GADT.
int_index
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.