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'')