scala - reales - ¿Cuáles son algunos ejemplos de programación de tipo de nivel?

manual android studio avanzado

Question

No entiendo qué significa "programación a nivel de tipo", ni puedo encontrar una explicación adecuada usando Google.

¿Podría alguien proporcionar un ejemplo que demuestre la programación a nivel de tipo? Las explicaciones y / o definiciones del paradigma serían útiles y apreciadas.

Answer 1

En la mayoría de los lenguajes estáticos, tiene dos "dominios", el nivel de valor y el nivel de tipo (algunos idiomas tienen incluso más). La programación de nivel implica la lógica de codificación (a menudo abstracción de funciones) en el sistema de tipos que se evalúa en tiempo de compilación. Algunos ejemplos serían metaprogramación de plantillas o familias de tipos Haskell.

Se necesitan algunas extensiones de idiomas para hacer este ejemplo en Haskell, pero de alguna manera las ignora por ahora y solo mira la familia de tipos como una función, pero sobre los números de nivel de tipo ( Nat ).

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits
import Data.Proxy

-- value-level
odd :: Integer -> Bool
odd 0 = False
odd 1 = True
odd n = odd (n-2)

-- type-level
type family Odd (n :: Nat) :: Bool where
    Odd 0 = False
    Odd 1 = True
    Odd n = Odd (n - 2)

test1 = Proxy :: Proxy (Odd 10)
test2 = Proxy :: Proxy (Odd 11)

Aquí, en lugar de probar si un valor de número natural es un número impar, estamos probando si un tipo de número natural es un número impar y lo reduce a un nivel de tipo Booleano en tiempo de compilación. Si evalúa este programa, los tipos de test1 y test2 se calculan en tiempo de compilación para:

λ: :type test1
test1 :: Proxy ''False
λ: :type test2
test2 :: Proxy ''True

Esa es la esencia de la programación a nivel de tipo, dependiendo del idioma, es posible que pueda codificar lógica compleja en el nivel de tipo que tiene una variedad de usos. Por ejemplo, para restringir cierto comportamiento en el nivel de valor, gestionar la finalización del recurso o almacenar más información sobre estructuras de datos.

Answer 2

Las otras respuestas son muy buenas, pero quiero enfatizar un punto. Nuestra teoría de términos del lenguaje de programación se basa en gran medida en el Cálculo Lambda. Un Lisp "puro" corresponde (más o menos) a un cálculo lambda no tipificado con mucho azúcar. El significado de los programas está definido por las reglas de evaluación que dicen cómo se reducen los términos del cálculo de Lambda a medida que se ejecuta el programa.

En un lenguaje escrito, asignamos tipos a términos. Para cada regla de evaluación, tenemos una regla de tipo correspondiente que muestra cómo la evaluación preserva los tipos. Dependiendo del sistema de tipo, también existen otras reglas que definen cómo los tipos se relacionan entre sí. ¡Resulta que una vez que obtienes un sistema de tipos suficientemente interesante, los tipos y su sistema de reglas también corresponden a una variante del Cálculo de Lambda!

Aunque es común pensar en Lambda Calculus como un lenguaje de programación ahora, originalmente fue diseñado como un sistema de lógica. Es por eso que es útil para razonar sobre los tipos de términos en un lenguaje de programación. Pero el aspecto del lenguaje de programación de Lambda Cálculo le permite a uno escribir programas que son evaluados por el verificador de tipos.

Con suerte, ahora puede ver que la "programación de tipo de nivel" no es sustancialmente diferente de la "programación de nivel de término", es solo que ahora no es muy común tener un lenguaje en un sistema de tipo que sea lo suficientemente potente como para tenerlo una razón para escribir programas en ella.

Answer 3

Ya está familiarizado con la programación de "nivel de valor", mediante la cual manipula valores como 42 :: Int o ''a'' :: Char . En lenguajes como Haskell o Scala, la programación a nivel de tipo le permite manipular tipos como Int :: * o Char :: * donde * es el tipo de un tipo concreto ( Maybe a o [a] son tipos concretos, pero no Maybe o [] que tienen kind * -> * ).

Considera esta función

foo :: Char -> Int
foo x = fromEnum x

Aquí foo toma un valor de tipo Char y devuelve un nuevo valor de tipo Int usando la instancia Enum para Char . Esta función manipula valores.

Ahora compare foo con esta familia de tipos, habilitada con la extensión de lenguaje TypeFamilies .

type family Foo (x :: *)
type instance Foo Char = Int

Aquí Foo toma un tipo de tipo * y devuelve un nuevo tipo de tipo * usando el simple mapeo Char -> Int . Esta es una función de nivel de tipo que manipula tipos.

Este es un ejemplo muy simple y podría preguntarse cómo esto podría ser útil. Usando herramientas de lenguaje más potentes, podemos comenzar a codificar pruebas de la corrección de nuestro código en el nivel de tipo (para más información sobre esto, consulte la correspondencia de Curry-Howard ).

Un ejemplo práctico es un árbol rojo-negro que usa programación de nivel de tipo para garantizar estáticamente que se mantienen las invariantes del árbol.

Un árbol rojo-negro tiene las siguientes propiedades simples:

1. Un nodo es rojo o negro.
2. La raíz es negra.
3. Todas las hojas son negras. (Todas las hojas son del mismo color que la raíz).
4. Cada nodo rojo debe tener dos nodos secundarios negros. Cada ruta desde un nodo dado a cualquiera de sus hojas descendientes contiene el mismo número de nodos negros.

Usaremos DataKinds y GADTs , una combinación de programación de nivel de tipo muy poderosa.

{-# LANGUAGE DataKinds, GADTS, KindSignatures #-}

import GHC.TypeLits

Primero, algunos tipos para representar los colores.

data Colour = Red | Black -- promoted to types via DataKinds

esto define un nuevo tipo de Colour habitado por dos tipos: Red y Black . Tenga en cuenta que no hay valores (ignorando fondos) que habitan estos tipos, pero no vamos a necesitarlos de todos modos.

Los nodos de árbol rojo-negro están representados por el siguiente GADT

-- ''c'' is the Colour of the node, either Red or Black
-- ''n'' is the number of black child nodes, a type level Natural number
-- ''a'' is the type of the values this node contains
data Node (c :: Colour) (n :: Nat) a where
    -- all leaves are black
    Leaf :: Node Black 1 a
    -- black nodes can have children of either colour
    B    :: Node l     n a -> a -> Node r     n a -> Node Black (n + 1) a
    -- red nodes can only have black children
    R    :: Node Black n a -> a -> Node Black n a -> Node Red n a

GADT nos permite expresar el Colour de los constructores R y B directamente en los tipos.

La raíz del árbol se ve así

data RedBlackTree a where
    RBTree :: Node Black n a -> RedBlackTree a

Ahora es imposible crear un RedBlackTree bien tipado que viole cualquiera de las 4 propiedades mencionadas anteriormente.

1. La primera restricción es obviamente cierta, solo hay 2 tipos que habitan Colour .
2. De la definición de RedBlackTree la raíz es negra.
3. A partir de la definición del constructor Leaf , todas las hojas son negras.
4. A partir de la definición del constructor R , ambos deben ser nodos Black . Además, el número de nodos secundarios negros de cada subárbol es igual (el mismo n se usa en el tipo de subárboles izquierdo y derecho)

El GHC comprueba todas estas condiciones en tiempo de compilación, lo que significa que nunca obtendremos una excepción en tiempo de ejecución de un código que no funciona correctamente que invalide nuestras suposiciones sobre un árbol rojo-negro. Es importante destacar que no hay costos de tiempo de ejecución asociados con estos beneficios adicionales, todo el trabajo se realiza en tiempo de compilación.