haskell - ¿Cómo pueden los tipos de cociente ayudar a exponer de forma segura los módulos internos?

functional-programming type-systems

Question

Al leer sobre los tipos de cociente y su uso en la programación funcional, me encontré con esta publicación . El autor menciona Data.Set como un ejemplo de un módulo que proporciona una tonelada de funciones que necesitan acceso a las partes internas del módulo:

Data.Set tiene 36 funciones, cuando todo lo que realmente se necesita para asegurar el significado de un conjunto ("Estos elementos son distintos") es toList y fromList .

El punto del autor parece ser que necesitamos "abrir el módulo y romper la abstracción" si olvidamos alguna función que se puede implementar de manera eficiente utilizando solo los elementos internos del módulo.

Luego dice

Podríamos aliviar todo este lío con tipos de cocientes.

pero no da ninguna explicación a esa afirmación.

Así que mi pregunta es: ¿cómo ayudan los tipos de cociente aquí?

EDITAR

He investigado un poco más y encontré un artículo "Construyendo programas polimórficos con tipos de cociente" . Se elabora sobre la declaración de recipientes de cociente y menciona la palabra "eficiente" en resumen e introducción. Pero si no he leído mal, no da ningún ejemplo de una representación eficiente que "oculte detrás" de un contenedor de cociente.

Editar 2

Un poco más se revela en el documento "[PDF] Programación en Teoría del Tipo de Homotopía" en el Capítulo 3. Se utiliza el hecho de que el tipo de cociente se puede implementar como una suma dependiente. Se introducen puntos de vista sobre los tipos abstractos (que me parecen muy similares a las clases de tipos) y se proporciona algún código Agda relevante. Sin embargo, el capítulo se centra en el razonamiento sobre los tipos abstractos , así que no estoy seguro de cómo se relaciona esto con mi pregunta.

Answer 1

Daré un ejemplo más simple donde está razonablemente claro. Es cierto que yo mismo realmente no veo cómo esto se traduciría en algo como Set , de manera eficiente.

data Nat = Nat (Integer / abs)

Para usar esto de manera segura, debemos asegurarnos de que cualquier función Nat -> T (con alguna Nat -> T no cociente, por razones de simplicidad) no dependa del valor entero real, sino solo de su valor absoluto . Para hacerlo, no es realmente necesario ocultar Integer completamente; sería suficiente para evitar que te pongas en contacto directamente. En su lugar, el compilador podría reescribir las coincidencias, por ejemplo,

even'' :: Nat -> Bool
even'' (Nat 0) = True
even'' (Nat 1) = False
even'' (Nat n) = even'' . Nat $ n - 2

podría ser reescrito a

even'' (Nat n'') = case abs n'' of
[|abs 0|] -> True
[|abs 1|] -> False
n -> even'' . Nat $ n - 2

Tal reescritura señalaría violaciones de equivalencia, por ejemplo,

bad (Nat 1) = "foo"
bad (Nat (-1)) = "bar"
bad _ = undefined

reescribiría a

bad (Nat n'') = case n'' of
1 -> "foo"
1 -> "bar"
_ -> undefined

que es obviamente un patrón superpuesto.

Answer 2

Descargo de responsabilidad: acabo de leer sobre los tipos de cociente al leer esta pregunta.

Creo que el autor acaba de decir que los conjuntos se pueden describir como tipos de cocientes en las listas. Es decir: (inventando una sintaxis similar a un haskell):

data Set a = Set [a] / (sort . nub) deriving (Eq)

Es decir, un Set a es solo un [a] con igualdad entre dos Set a determinado por la sort . nub sort . nub subyacentes de las listas son iguales.

Podríamos hacer esto explícitamente así, supongo:

import Data.List
data Set a = Set [a] deriving (Show)
instance (Ord a, Eq a) => Eq (Set a) where
(Set xs) == (Set ys) = (sort $ nub xs) == (sort $ nub ys)

No estoy seguro de si esto es realmente lo que pretendía el autor, ya que no es una forma particularmente eficaz de implementar un conjunto. Alguien puede sentirse libre de corregirme.

Answer 3

Hace poco hice una publicación en el blog sobre tipos de cocientes y un comentario me condujo hasta aquí. La publicación del blog puede proporcionar algún contexto adicional además de los documentos a los que se hace referencia en la pregunta.

La respuesta es en realidad bastante sencilla. Una forma de llegar a esto es hacer la pregunta: ¿por qué estamos usando un tipo de datos abstractos en primer lugar para Data.Set ?

Hay dos razones distintas y separables. La primera razón es ocultar el tipo interno detrás de una interfaz para que podamos sustituir un tipo completamente nuevo en el futuro. El segundo motivo es imponer invariantes implícitos en los valores del tipo interno. El tipo de cociente y sus tipos de subconjuntos duales nos permiten hacer explícitos y exigidos por el verificador de tipos para que ya no tengamos que ocultar la representación. Así que permítanme ser muy claro: los tipos de cociente (y subconjunto) no le proporcionan ningún tipo de ocultación de implementación. Si implementa Data.Set con tipos de cociente usando listas como su representación, luego decide que desea usar árboles, deberá cambiar todo el código que usa su tipo.

Comencemos con un ejemplo más simple (leftaroundabout''s). Haskell tiene un tipo Integer pero no un tipo Natural . Una forma sencilla de especificar Natural como un tipo de subconjunto utilizando la sintaxis creada sería:

type Natural = { n :: Integer | n >= 0 }

Podríamos implementar esto como un tipo abstracto usando un constructor inteligente que arrojó un error cuando se le dio un Integer negativo. Este tipo dice que solo un subconjunto de los valores de tipo Integer son válidos. Otro enfoque que podríamos usar para implementar este tipo es usar un tipo de cociente:

type Natural = Integer / ~ where n ~ m = abs n == abs m

Cualquier función h :: X -> T para algún tipo T induce un tipo de cociente en X cocido por la relación de equivalencia x ~ y = hx == hy . Los tipos de cociente de este formulario se codifican más fácilmente como tipos de datos abstractos. En general, sin embargo, puede que no haya una función tan conveniente, por ejemplo:

type Pair a = (a, a) / ~ where (a, b) ~ (x, y) = a == x && b == y || a == y && b == x

(En cuanto a cómo se relacionan los tipos de cociente con los setoides, un tipo de cociente es un setoide que obliga a respetar su relación de equivalencia). Por ejemplo, esta segunda definición de Natural tiene la propiedad de que hay dos valores que representan 2 . A saber, 2 y -2 . El aspecto del tipo de cociente dice que se nos permite hacer lo que queramos con el Integer subyacente, siempre y cuando nunca produzcamos un resultado que diferencie entre estos dos representantes. Otra forma de ver esto es que podemos codificar un tipo de cociente usando tipos de subconjuntos como:

X/~ = forall a. { f :: X -> a | forEvery (/(x, y) -> x ~ y ==> f x == f y) } -> a

Desafortunadamente, eso para forEvery equivale a verificar la igualdad de funciones.

Al alejarse, los tipos de subconjuntos agregan restricciones a los productores de valores y los tipos de cocientes agregan restricciones a los consumidores de valores. Las invariantes aplicadas por un tipo de datos abstractos pueden ser una mezcla de estos. De hecho, podemos decidir representar un Set la siguiente manera:

data Tree a = Empty | Branch (Tree a) a (Tree a)
type BST a = { t :: Tree a | isSorted (toList t) }
type Set a = { t :: BST a | noDuplicates (toList t) } / ~
where s ~ t = toList s == toList t

Tenga en cuenta que nada de esto requiere que isSorted , noDuplicates o toList . "Simplemente" necesitamos convencer al verificador de tipos de que las implementaciones de funciones en este tipo satisfacen estos predicados. El tipo de cociente nos permite tener una representación redundante al tiempo que nos obliga a tratar las representaciones equivalentes de la misma manera. Esto no significa que no podamos aprovechar la representación específica que tenemos para producir un valor, solo significa que debemos convencer al comprobador de tipos de que habríamos producido el mismo valor si se hubiera dado una representación diferente y equivalente. Por ejemplo:

maximum :: Set a -> a
maximum s = exposing s as t in go t
where go Empty = error "maximum of empty Set"
go (Branch _ x Empty) = x
go (Branch _ _ r) = go r

La obligación de prueba de esto es que el elemento más a la derecha de cualquier árbol de búsqueda binario con los mismos elementos es el mismo. Formalmente, se go t == go t'' siempre que se toList t == toList t'' . Si utilizáramos una representación que garantizaba que el árbol estaría equilibrado, por ejemplo, un árbol AVL, esta operación sería O(log N) al convertir a una lista y seleccionar el máximo de la lista sería O(N) . Incluso con esta representación, este código es estrictamente más eficiente que convertir a una lista y obtener el máximo de la lista. Tenga en cuenta que no se pudo implementar una función que muestre la estructura de árbol del Set . Tal función sería mal escrita.