haskell - Cómo agregar una restricción a un constructor de tipos
servant (1)
Considere el siguiente tipo de datos:
data Get (statusCode :: Nat)
En realidad, es un constructor de tipo simplificado de servidor que luego se usa en una API de nivel de tipo como esta:
type API = "users" :> Verb ''GET 200 ''[JSON] [User]
Para nuestros propósitos podemos reducir la API para
type API = Get 200
Ahora, tener una restricción del código de estado de tipo Nat es demasiado flojo, lo que permite definir un código de estado HTTP no existente:
type API = Get 999
Por lo tanto, la pregunta: ¿Hay una manera de restringir el conjunto de naturales que se pueden aplicar al constructor de tipo Get ?
Lo que se intentó
Omitiré todos los pragmas e importaciones en los ejemplos de código para mayor claridad.
Un tipo diferente para statusCode
Una forma obvia de solucionarlo sería definir un ADT separado para los códigos de estado y usarlo en lugar de Nat utilizando la promoción de tipos de datos.
data StatusCode = HTTP200 | HTTP201 | HTTP202
data Get (statusCode :: StatusCode)
Sin embargo, este es un cambio de última hora, que requeriría golpear una versión principal y volver a escribir todas las definiciones de los usuarios. Dudo que el beneficio de los códigos restringidos valga la pena.
DatatypeContexts
Esta extensión permite tener una restricción directa en nuestra variable de tipo
data IsStatusCode statusCode => Get (statusCode :: Nat)
pero requiere que los usuarios agreguen la restricción a toda su declaración. De nuevo, un cambio de ruptura. Además, DatatypeContexts está en desuso.
Tipo Familias
Podríamos crear condicionalmente Get'' partir del siguiente ejemplo utilizando familias de tipos, pero por alguna razón, la declaración de un alias de tipo se compila alegremente. Para obtener un error necesitamos construir un valor de este tipo, que también es un cambio importante.
data Get'' (statusCode :: Nat) = Get
type family Get x where
Get x = If (x <=? 600) (Get'' x) (TypeError (Text "Invalid Code"))
type API1 = Get 200
type API2 = Get 999 -- compiles.
api :: Get 999 -- doesn''t compile.
api = Get
Comenzaré con una solución, luego discutiré las otras posibilidades (que parecen no haberse realizado):
{-# LANGUAGE TypeOperators, TypeInType, GADTs #-}
import GHC.TypeLits (Nat, type (<=))
import Data.Proxy (Proxy(..))
import Data.Kind (type (*))
data Get (statusCode :: Nat) :: (statusCode <= 600) => *
type API1 = Get 900 -- compiles
type API2 = Get 200 -- compiles
api1 :: Proxy (Get 900) -- doesn''t compile
api1 = Proxy
api2 :: Proxy (Get 200) -- compiles
api2 = Proxy
No se necesitan familias de tipos, no hay necesidad de bajar nunca al nivel de valor. Los sinónimos de tipo, sin embargo, compilarán bien. El uso de un sinónimo de tipo de un Get no válido provocará un bloqueo del tiempo de compilación en el sitio de uso. Considero que esta es una solución tan buena como se puede esperar. Por favor, hágamelo saber si algo no está claro.
A continuación, solo algunas reflexiones sobre los otros enfoques:
DatatypeContexts
Éste nunca funcionará: además de estar en desuso, todo lo que hace es agregar la restricción a los constructores. Usted indicó específicamente que no quiere tener que construir nada del tipo, por lo que esto no tiene sentido. La nueva sintaxis de GADT corrige esta ambigüedad: las restricciones ahora están claramente vinculadas a los constructores de datos o tipos.
Tipo Familias y TypeError
Creo que esto debería funcionar, y sin tener que construir un valor del tipo. (Así que lo siguiente debería estar bien :)
data Get'' (statusCode :: Nat)
type family Get x where
Get x = If (x <=? 600) (Get'' x) (TypeError (Text "Invalid Code"))
api2 :: Proxy (Get 200) -- should compile.
api2 = Proxy
api1 :: Proxy (Get 999) -- shouldn''t compile, but currently does
api1 = Proxy
Estoy motivado para creer que esto debería funcionar en base al example de este marcador de rastreo. Claramente, algo aquí no se comporta como debería: incluso si sustituyo la llamada a la función de tipo If con el propio TypeError , aún no se activa nada, parece que los TypeErrors que no son de nivel superior todavía causan algunos problemas.
Por otro lado, no estoy realmente seguro de cuál debería ser el comportamiento de TypeError en los sinónimos de type , aunque me inclino a decir que el type API1 = Get 999 no debería compilarse, ya que type API1 = TypeError (Text "error") doesn '' t