haskell - ¿Puedo proporcionar al comprobador de tipos pruebas sobre los productos naturales inductivos en GHC 7.6?

data-kinds

Question

GHC 7.6.1 viene con nuevas características para la programación a nivel de tipo, incluida la promoción de tipo de datos . Tomando el ejemplo sobre los tipos naturales y vectores a partir de ahí, me gustaría poder escribir funciones en vectores que se basan en leyes básicas de la aritmética.

Desafortunadamente, a pesar de que las leyes que quiero son generalmente fáciles de probar en inductivos naturales mediante el análisis de casos y la inducción, dudo que pueda convencer al tipo-verificador de esto. Como ejemplo simple, la comprobación de tipo de la función inversa ingenua a continuación requiere una prueba de que n + Su Ze ~ Su n .

¿Hay alguna forma en que pueda proporcionar esa prueba, o estoy realmente en el reino de los tipos dependientes en toda regla ahora?

{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeFamilies, TypeOperators #-}

data Nat = Ze | Su Nat

data Vec :: * -> Nat -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

type family (m :: Nat) + (n :: Nat) :: Nat

type instance Ze + n = n
type instance (Su m + n) = Su (m + n)

append :: Vec a m -> Vec a n -> Vec a (m + n)
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

rev :: Vec a n -> Vec a n
rev Nil = Nil
rev (Cons x xs) = rev xs `append` Cons x Nil

Answer 1

(Nota: solo he verificado el tipo de este código).

Enfoque 1

En realidad, puedes manipular pruebas almacenándolas en GADTs. Deberá activar ScopedTypeVariables para que este enfoque funcione.

data Proof n where
    NilProof  :: Proof Ze
    ConsProof :: (n + Su Ze) ~ Su n => Proof n -> Proof (Su n)

class PlusOneIsSucc n where proof :: Proof n
instance PlusOneIsSucc Ze where proof = NilProof
instance PlusOneIsSucc n => PlusOneIsSucc (Su n) where
    proof = case proof :: Proof n of
        NilProof    -> ConsProof proof
        ConsProof _ -> ConsProof proof

rev :: PlusOneIsSucc n => Vec a n -> Vec a n
rev = go proof where
    go :: Proof n -> Vec a n -> Vec a n
    go NilProof Nil = Nil
    go (ConsProof p) (Cons x xs) = go p xs `append` Cons x Nil

En realidad, tal vez la motivación interesante para el tipo de Proof anterior, originalmente tenía

data Proof n where Proof :: (n + Su Ze) ~ Su n => Proof n

Pero, esto no funcionó: GHC se quejó con razón de que solo porque sabemos (Su n)+1 = Su (Su n) no implica que sepamos n+1 = Su n , que es lo que necesitamos saber para Hacer la llamada recursiva a rev en el caso Cons . Así que tuve que expandir el significado de una Proof para incluir una prueba de todas las ecuaciones para los naturales hasta e incluyendo n , esencialmente algo similar al proceso de fortalecimiento al pasar de la inducción a la fuerte inducción.

Enfoque 2

Después de un poco de reflexión, me di cuenta de que resulta que la clase es un poco superflua; eso hace que este enfoque sea especialmente bueno, ya que no requiere extensiones adicionales (incluso ScopedTypeVariables ) y no introduce restricciones adicionales al tipo de Vec .

data Proof n where
    NilProof  :: Proof Ze
    ConsProof :: (n + Su Ze) ~ Su n => Proof n -> Proof (Su n)

proofFor :: Vec a n -> Proof n
proofFor Nil = NilProof
proofFor (Cons x xs) = let rec = proofFor xs in case rec of
    NilProof    -> ConsProof rec
    ConsProof _ -> ConsProof rec

rev :: Vec a n -> Vec a n
rev xs = go (proofFor xs) xs where
    go :: Proof n -> Vec a n -> Vec a n
    go NilProof Nil = Nil
    go (ConsProof p) (Cons x xs) = go p xs `append` Cons x Nil

Enfoque 3

Alternativamente, si cambia la implementación de rev a bit a contras el último elemento en el segmento inicial invertido de la lista, entonces el código puede parecer un poco más directo. (Este enfoque tampoco requiere extensiones adicionales).

class Rev n where
    initLast :: Vec a (Su n) -> (a, Vec a n)
    rev :: Vec a n -> Vec a n

instance Rev Ze where
    initLast (Cons x xs) = (x, xs)
    rev x = x

instance Rev n => Rev (Su n) where
    initLast (Cons x xs) = case initLast xs of
        (x'', xs'') -> (x'', Cons x xs'')
    rev as = case initLast as of
        (a, as'') -> Cons a (rev as'')

Enfoque 4

Al igual que el enfoque 3, pero nuevamente observando que las clases de tipos no son necesarias.

initLast :: Vec a (Su n) -> (a, Vec a n)
initLast (Cons x xs) = case xs of
    Nil     -> (x, Nil)
    Cons {} -> case initLast xs of
        (x'', xs'') -> (x'', Cons x xs'')

rev :: Vec a n -> Vec a n
rev Nil = Nil
rev xs@(Cons {}) = case initLast xs of
    (x, xs'') -> Cons x (rev xs'')