Haskell nivel de nivel literal Nat: estado?

dependent-type

Question

GHC tiene nats de nivel de tipo literal. Puedo leer algunas cosas sobre ellos, por ejemplo, aquí:

https://ghc.haskell.org/trac/ghc/wiki/TypeNats

Desafortunadamente, parece que hay poca documentación sobre ellos, y casi nada de lo que trato de hacer realmente funciona.

El comentario 18 de esta página menciona este ejemplo simple de Vecs parametrizados por tamaño (he agregado pragmas de IDIOMA y una declaración de importación):

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

import GHC.TypeLits

data Vec :: Nat -> * -> * where
  Nil  :: Vec 0 a
  (:>) :: a -> Vec n a -> Vec (n+1) a

(+++) :: Vec n a -> Vec m a -> Vec (n+m) a
Nil       +++ bs = bs
(a :> as) +++ bs = a :> (as +++ bs)

No estaba funcionando en ese momento, pero luego la implementación supuestamente se modificó para que esto funcionara. Eso fue hace 5 años ... pero no funciona en mi GHC 7.10.1:

trash.hs:15:20:
    Could not deduce ((n + m) ~ ((n1 + m) + 1))
    from the context (n ~ (n1 + 1))
      bound by a pattern with constructor
                 :> :: forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a,
               in an equation for ‘+++’
      at trash.hs:15:2-8
    NB: ‘+’ is a type function, and may not be injective
    Expected type: Vec (n + m) a
      Actual type: Vec ((n1 + m) + 1) a
    Relevant bindings include
      bs :: Vec m a (bound at trash.hs:15:15)
      as :: Vec n1 a (bound at trash.hs:15:7)
      (+++) :: Vec n a -> Vec m a -> Vec (n + m) a
        (bound at trash.hs:14:1)
    In the expression: a :> (as +++ bs)
    In an equation for ‘+++’: (a :> as) +++ bs = a :> (as +++ bs)

¿Cuál es el problema aquí? ¿Se supone que los nats de nivel de tipo se pueden utilizar para este tipo de cosas? Si es así, ¿cómo implemento la función (+++)? Si no, ¿cuál es su caso de uso?

Answer 1

Como los comentaristas han mencionado, el typechecker actualmente no puede descargar esta igualdad porque requiere álgebra. Mientras que usted y yo sabemos que n + m = n1 + m + 1 dado n = n1 + 1 , nadie ha enseñado al verificador de tipos de GHC cómo realizar ese tipo de aritmética. En idiomas como Ada, Idris o Coq, usted podría enseñarle al compilador estas reglas o tal vez las reglas de la aritmética se le proporcionarán en una biblioteca, pero en Haskell el typechecker es un poco más rígido (pero mucho más amigable a la programación del mundo real, en mi opinión) y, lamentablemente, hay que recurrir a un complemento de comprobación de tipos.

La persona que conozco que es la más activa en este problema es Iavor Diatchki . Ese documento está detrás del estúpido muro de pagos de ACM, pero puede encontrar su charla sobre Haskell Symposium 2015 aquí en YouTube , ¡está muy bien explicado! Su charla usa el mismo ejemplo que el tuyo, el vector siempre popular. Su sucursal en el repositorio de GHC trabaja en fusionarla en la línea principal de GHC, pero hasta donde sé no hay fechas establecidas. Por ahora tienes que usar el complemento typechecker, que no es tan malo. Después de todo, el objetivo original de Plugins / Typechecker era permitir un trabajo interesante como este sin tener que combinar todo en el código fuente. ¡Hay algo que decir para la modularidad!