stay servants personajes night mejores guia grand femeninos fate anime haskell types data-kinds

haskell - servants - fate stay night



¿Cuáles son todos los mecanismos utilizados para habilitar la API basada en el tipo de Servant? (1)

Mirar el documento de Servant para una explicación completa puede ser la mejor opción. Sin embargo, intentaré ilustrar el enfoque adoptado por Servant aquí, implementando "TinyServant", una versión de Servant reducida al mínimo.

Siento que esta respuesta sea tan larga. Sin embargo, todavía es un poco más corto que el papel, y el código que se discute aquí es "solo" 81 líneas, disponible también como archivo de Haskell here .

Preparativos

Para empezar, aquí están las extensiones de idioma que necesitaremos:

{-# LANGUAGE DataKinds, PolyKinds, TypeOperators #-} {-# LANGUAGE TypeFamilies, FlexibleInstances, ScopedTypeVariables #-} {-# LANGUAGE InstanceSigs #-}

Los tres primeros son necesarios para la definición del propio DSL de nivel de tipo. El DSL hace uso de cadenas de nivel de tipo ( DataKinds ) y también utiliza polimorfismo tipo ( PolyKinds ). El uso de los operadores de infijo de nivel de tipo tales como :<|> y :> requiere la extensión TypeOperators .

Los segundos tres son necesarios para la definición de la interpretación (definiremos algo que recuerde a lo que hace un servidor web, pero sin la parte web completa). Para esto, necesitamos funciones de tipo de tipo ( TypeFamilies ), alguna programación de clase de tipo que requerirá ( FlexibleInstances ), y algunas anotaciones de tipo para guiar el verificador de tipo que requiere ScopedTypeVariables .

Sólo con fines de documentación, también utilizamos InstanceSigs .

Aquí está nuestro encabezado de módulo:

module TinyServant where import Control.Applicative import GHC.TypeLits import Text.Read import Data.Time

Después de estos preliminares, estamos listos para empezar.

Especificaciones API

El primer ingrediente es definir los tipos de datos que se están utilizando para las especificaciones de la API.

data Get (a :: *) data a :<|> b = a :<|> b infixr 8 :<|> data (a :: k) :> (b :: *) infixr 9 :> data Capture (a :: *)

Definimos solo cuatro constructos en nuestro lenguaje simplificado:

  1. A Get a representación y un punto final de tipo a (de tipo * ). En comparación con el Servidor completo, ignoramos los tipos de contenido aquí. Necesitamos el tipo de datos solo para las especificaciones API. Ahora hay valores directamente correspondientes, y por lo tanto no hay un constructor para Get .

  2. Con a :<|> b , representamos la elección entre dos rutas. Nuevamente, no necesitaríamos un constructor, pero resulta que usaremos un par de manejadores para representar al manejador de una API usando :<|> . Para aplicaciones anidadas de :<|> , obtendríamos pares de manejadores anidados, que se ven un poco feos al usar la notación estándar en Haskell, por lo que definimos que el constructor :<|> es equivalente a un par.

  3. Con item :> rest , representamos rutas anidadas, donde item es el primer componente y rest son los componentes restantes. En nuestro DSL simplificado, solo hay dos posibilidades para el item : una cadena de nivel de tipo o una Capture . Como las cadenas de nivel de tipo son de tipo Symbol , pero una Capture , que se define a continuación, es de tipo * , creamos el primer argumento de :> tipo polimórfico , para que ambas opciones sean aceptadas por el sistema de tipo Haskell.

  4. A Capture a representa un componente de ruta que se captura, analiza y luego se expone al controlador como un parámetro de tipo a . En Servidor completo, Capture tiene una cadena adicional como parámetro que se utiliza para la generación de documentación. Aquí omitimos la cadena.

API de ejemplo

Ahora podemos escribir una versión de la especificación de la API a partir de la pregunta, adaptada a los tipos reales que se Data.Time en Data.Time y a nuestro DSL simplificado:

type MyAPI = "date" :> Get Day :<|> "time" :> Capture TimeZone :> Get ZonedTime

La interpretación como servidor

El aspecto más interesante es, por supuesto, lo que podemos hacer con la API, y en eso consiste principalmente la pregunta.

Servant define varias interpretaciones, pero todas siguen un patrón similar. Aquí definiremos uno, que está inspirado en la interpretación como un servidor web.

En Servant, la función de servidor toma un proxy para el tipo de API y un manejador que coincide con el tipo de API con una Application WAI, que es esencialmente una función de las solicitudes HTTP a las respuestas. Nos abstraeremos de la parte web aquí, y definiremos

serve :: HasServer layout => Proxy layout -> Server layout -> [String] -> IO String

en lugar.

La clase HasServer , que definiremos a continuación, tiene instancias para todas las diferentes construcciones del DSL de nivel de tipo y, por lo tanto, codifica lo que significa que un layout tipo Haskell pueda interpretarse como un tipo de API de un servidor.

El Proxy hace una conexión entre el tipo y el nivel de valor. Se define como

data Proxy a = Proxy

y su único propósito es que al pasar a un constructor Proxy con un tipo explícitamente especificado, podemos hacerlo muy explícito para el tipo de API que queremos calcular el servidor.

El argumento del Server es el controlador para la API . Aquí, el propio Server es una familia de tipos, y calcula a partir del tipo de API el tipo que deben tener los manejadores. Este es un ingrediente central de lo que hace que Servant funcione correctamente.

La lista de cadenas representa la solicitud, reducida a una lista de componentes de URL. Como resultado, siempre devolvemos una respuesta de String y permitimos el uso de IO . Full Servant usa tipos algo más complicados aquí, pero la idea es la misma.

La familia de tipos de Server

Definimos Server como una familia de tipos primero. (En Servant, la familia de tipos que se está utilizando es ServerT , y se define como parte de la clase HasServer ).

type family Server layout :: *

El controlador para un Get a punto final es simplemente una acción IO que produce un a . (Una vez más, en el código completo de Servant, tenemos un poco más de opciones, como generar un error).

type instance Server (Get a) = IO a

El controlador para a :<|> b es un par de controladores, por lo que podríamos definir

type instance Server (a :<|> b) = (Server a, Server b) -- preliminary

Pero como se indicó anteriormente, para las apariciones anidadas de :<|> esto conduce a pares anidados, que se ven algo más agradables con un constructor de par de infijo, por lo que Servant define el equivalente

type instance Server (a :<|> b) = Server a :<|> Server b

Queda por explicar cómo se maneja cada uno de los componentes de la ruta.

Las cadenas literales en las rutas no afectan el tipo de manejador:

type instance Server ((s :: Symbol) :> r) = Server r

Sin embargo, una captura significa que el controlador espera un argumento adicional del tipo que se captura:

type instance Server (Capture a :> r) = a -> Server r

Cálculo del tipo de manejador de la API de ejemplo

Si expandimos el Server MyAPI , obtenemos

Server MyAPI ~ Server ("date" :> Get Day :<|> "time" :> Capture TimeZone :> Get ZonedTime) ~ Server ("date" :> Get Day) :<|> Server ("time" :> Capture TimeZone :> Get ZonedTime) ~ Server (Get Day) :<|> Server ("time" :> Capture TimeZone :> Get ZonedTime) ~ IO Day :<|> Server ("time" :> Capture TimeZone :> Get ZonedTime) ~ IO Day :<|> Server (Capture TimeZone :> Get ZonedTime) ~ IO Day :<|> TimeZone -> Server (Get ZonedTime) ~ IO Day :<|> TimeZone -> IO ZonedTime

Por lo tanto, según lo previsto, el servidor de nuestra API requiere un par de manejadores, uno que proporcione una fecha y uno que, dada una zona horaria, proporcione una hora. Podemos definir estos ahora mismo:

handleDate :: IO Day handleDate = utctDay <$> getCurrentTime handleTime :: TimeZone -> IO ZonedTime handleTime tz = utcToZonedTime tz <$> getCurrentTime handleMyAPI :: Server MyAPI handleMyAPI = handleDate :<|> handleTime

La clase HasServer

Todavía tenemos que implementar la clase HasServer , que tiene el siguiente aspecto:

class HasServer layout where route :: Proxy layout -> Server layout -> [String] -> Maybe (IO String)

La tarea de la route de la función es casi como serve . Internamente, tenemos que enviar una solicitud entrante al enrutador correcto. En el caso de :<|> , esto significa que tenemos que elegir entre dos manejadores. ¿Cómo hacemos esta elección? Una opción simple es permitir que la route falle, devolviendo un Maybe . (Una vez más, full Servant es algo más sofisticado aquí, y la versión 0.5 tendrá una estrategia de enrutamiento muy mejorada).

Una vez que tenemos la route definida, podemos definir fácilmente el serve en términos de route :

serve :: HasServer layout => Proxy layout -> Server layout -> [String] -> IO String serve p h xs = case route p h xs of Nothing -> ioError (userError "404") Just m -> m

Si ninguna de las rutas coincide, fallamos con un 404. De lo contrario, devolvemos el resultado.

Las instancias de HasServer

Para un punto final Get , definimos

type instance Server (Get a) = IO a

por lo tanto, el manejador es una acción de E / S que produce un a , que debemos convertir en una String . Usamos show para este propósito. En la implementación real de Servant, esta conversión es manejada por la maquinaria de tipos de contenido, y típicamente involucrará la codificación a JSON o HTML.

instance Show a => HasServer (Get a) where route :: Proxy (Get a) -> IO a -> [String] -> Maybe (IO String) route _ handler [] = Just (show <$> handler) route _ _ _ = Nothing

Dado que solo estamos emparejando un punto final, es necesario que la solicitud esté vacía en este punto. Si no lo es, esta ruta no coincide y devolvemos Nothing .

Veamos la elección siguiente:

instance (HasServer a, HasServer b) => HasServer (a :<|> b) where route :: Proxy (a :<|> b) -> (Server a :<|> Server b) -> [String] -> Maybe (IO String) route _ (handlera :<|> handlerb) xs = route (Proxy :: Proxy a) handlera xs <|> route (Proxy :: Proxy b) handlerb xs

Aquí, obtenemos un par de controladores y usamos <|> para Maybe para probar ambos.

¿Qué sucede para una cadena literal?

instance (KnownSymbol s, HasServer r) => HasServer ((s :: Symbol) :> r) where route :: Proxy (s :> r) -> Server r -> [String] -> Maybe (IO String) route _ handler (x : xs) | symbolVal (Proxy :: Proxy s) == x = route (Proxy :: Proxy r) handler xs route _ _ _ = Nothing

El controlador para s :> r es del mismo tipo que el controlador para r . Requerimos que la solicitud no esté vacía y que el primer componente coincida con la contraparte de nivel de valor de la cadena de nivel de tipo. Obtenemos la cadena de nivel de valor correspondiente al literal de cadena de nivel de tipo aplicando symbolVal . Para esto, necesitamos una restricción KnownSymbol en el literal de cadena de nivel de tipo. Pero todos los literales concretos en GHC son automáticamente una instancia de KnownSymbol .

El caso final es para capturas:

instance (Read a, HasServer r) => HasServer (Capture a :> r) where route :: Proxy (Capture a :> r) -> (a -> Server r) -> [String] -> Maybe (IO String) route _ handler (x : xs) = do a <- readMaybe x route (Proxy :: Proxy r) (handler a) xs route _ _ _ = Nothing

En este caso, podemos asumir que nuestro manejador es en realidad una función que espera un a . Requerimos que el primer componente de la solicitud sea analizable como a . Aquí, usamos Read , mientras que en Servidor, usamos nuevamente la maquinaria de tipo de contenido. Si la lectura falla, consideramos que la solicitud no coincide. De lo contrario, podemos alimentarlo al manejador y continuar.

Probando todo

Ahora hemos terminado.

Podemos confirmar que todo funciona en GHCi:

GHCi> serve (Proxy :: Proxy MyAPI) handleMyAPI ["time", "CET"] "2015-11-01 20:25:04.594003 CET" GHCi> serve (Proxy :: Proxy MyAPI) handleMyAPI ["time", "12"] *** Exception: user error (404) GHCi> serve (Proxy :: Proxy MyAPI) handleMyAPI ["date"] "2015-11-01" GHCi> serve (Proxy :: Proxy MyAPI) handleMyAPI [] *** Exception: user error (404)

Estoy muy desconcertado por cómo Servant es capaz de lograr la magia que hace al escribir. El ejemplo en el sitio web ya me desconcierta enormemente:

type MyAPI = "date" :> Get ''[JSON] Date :<|> "time" :> Capture "tz" Timezone :> Get ''[JSON] Time

Obtengo la "fecha", "hora", [JSON] y "tz" son literales de nivel de tipo. Son valores que se han "convertido" en tipos. Bueno.

Entiendo que :> y :<|> son operadores de tipo. Bueno.

No entiendo cómo estas cosas, una vez que se han convertido en tipos, se pueden extraer de nuevo en valores. ¿Cuál es el mecanismo para hacer esto?

Tampoco entiendo cómo la primera parte de este tipo puede obtener el marco para esperar una función de la IO Date de la firma, o cómo la segunda parte de este tipo puede obtener el marco para esperar una función de la zona Timezone -> IO Time de la firma Timezone -> IO Time de mi parte. ¿Cómo se produce esta transformación?

¿Y cómo puede entonces el marco llamar a una función para la cual inicialmente no conocía el tipo?

Estoy seguro de que hay varias extensiones de GHC y características únicas en juego aquí con las que no estoy familiarizado y que se combinan para hacer que esta magia suceda.

¿Alguien puede explicar qué características están involucradas aquí y cómo están trabajando juntas?