¿El sistema de tipos de Haskell es formalmente equivalente al de Java? [cerrado]

66

Me doy cuenta de que algunas cosas son más fáciles / difíciles en un idioma que en el otro, pero solo me interesan las características relacionadas con el tipo que son posibles en uno e imposibles / irrelevantes en el otro. Para hacerlo más específico, ignoremos las extensiones de tipo Haskell ya que hay tantas que hacen todo tipo de cosas locas / geniales.

GlenPeterson
fuente
44
Yo también tengo curiosidad por escuchar a los teóricos de categoría largamente respondidos a esta pregunta; Aunque dudo que lo entienda particularmente, todavía estoy interesado en un detalle de esto. Mi inclinación por las cosas que he leído es que el sistema de tipos HM permite que el compilador sepa mucho sobre lo que hace su código, razón por la cual es capaz de inferir tipos y ofrecer tantas garantías sobre el comportamiento. Pero ese es solo mi instinto y estoy seguro de que hay otras cosas que desconozco por completo.
Jimmy Hoffa
1
Esta es una gran pregunta: ¡es hora de twittear a los seguidores para el gran debate de Haskell / JVM!
Martijn Verburg
66
@ m3th0dman: Scala tiene exactamente el mismo soporte para funciones de orden superior que Java. En Scala, las funciones de primera clase se representan simplemente como instancias de clases abstractas con un único método abstracto, al igual que Java. Claro, Scala tiene azúcar sintáctica para definir estas funciones, y tiene una biblioteca estándar rica de tipos de funciones predefinidos y métodos que aceptan funciones, pero desde la perspectiva del sistema de tipos , de eso se trata esta pregunta, no hay diferencia . Entonces, si Scala puede hacerlo, entonces Java también puede hacerlo, y de hecho hay bibliotecas FP inspiradas en Haskell para Java.
Jörg W Mittag
2
@ m3th0dman: De eso no se trata esta pregunta.
Phil
77
@ m3th0dman Son tipos perfectamente normales. Las listas no tienen nada de especial, excepto algunas sutilezas sinácticas. Puede definir fácilmente su propio tipo de datos algebraicos que sea equivalente al tipo de lista incorporado, excepto por la sintaxis literal y los nombres de los constructores.
sepp2k

Respuestas:

63

("Java", como se usa aquí, se define como Java SE 7 estándar ; "Haskell", como se usa aquí, se define como Haskell 2010 estándar ).

Cosas que tiene el sistema de tipos de Java pero que Haskell no:

  • subtipo nominal polimorfismo
  • información de tipo de tiempo de ejecución parcial

Cosas que tiene el sistema de tipos de Haskell pero que Java no tiene:

  • polimorfismo ad-hoc acotado
    • da lugar a un polimorfismo de subtipo "basado en restricciones"
  • polimorfismo paramétrico de tipo superior
  • mecanografía principal

EDITAR:

Ejemplos de cada uno de los puntos enumerados anteriormente:

Exclusivo de Java (en comparación con Haskell)

Subtipo nominal de polimorfismo

/* declare explicit subtypes (limited multiple inheritance is allowed) */
abstract class MyList extends AbstractList<String> implements RandomAccess {

    /* specify a type's additional initialization requirements */
    public MyList(elem1: String) {
        super() /* explicit call to a supertype's implementation */
        this.add(elem1) /* might be overridden in a subtype of this type */
    }

}

/* use a type as one of its supertypes (implicit upcasting) */
List<String> l = new ArrayList<>() /* some inference is available for generics */

Información de tipo de tiempo de ejecución parcial

/* find the outermost actual type of a value at runtime */
Class<?> c = l.getClass // will be 'java.util.ArrayList'

/* query the relationship between runtime and compile-time types */
Boolean b = l instanceOf MyList // will be 'false'

Exclusivo de Haskell (en comparación con Java)

Polimorfismo ad-hoc acotado

-- declare a parametrized bound
class A t where
  -- provide a function via this bound
  tInt :: t Int
  -- require other bounds within the functions provided by this bound
  mtInt :: Monad m => m (t Int)
  mtInt = return tInt -- define bound-provided functions via other bound-provided functions

-- fullfill a bound
instance A Maybe where
  tInt = Just 5
  mtInt = return Nothing -- override defaults

-- require exactly the bounds you need (ideally)
tString :: (Functor t, A t) => t String
tString = fmap show tInt -- use bounds that are implied by a concrete type (e.g., "Show Int")

Polimorfismo de subtipo "basado en restricciones" (basado en polimorfismo ad-hoc acotado)

-- declare that a bound implies other bounds (introduce a subbound)
class (A t, Applicative t) => B t where -- bounds don't have to provide functions

-- use multiple bounds (intersection types in the context, union types in the full type)
mtString :: (Monad m, B t) => m (t String)
mtString = return mtInt -- use a bound that is implied by another bound (implicit upcasting)

optString :: Maybe String
optString = join mtString -- full types are contravariant in their contexts

Polimorfismo paramétrico de tipo superior

-- parametrize types over type variables that are themselves parametrized
data OneOrTwoTs t x = OneVariableT (t x) | TwoFixedTs (t Int) (t String)

-- bounds can be higher-kinded, too
class MonadStrip s where
  -- use arbitrarily nested higher-kinded type variables
  strip :: (Monad m, MonadTrans t) => s t m a -> t m a -> m a

Mecanografía principal

Es difícil dar un ejemplo directo de este, pero significa que cada expresión tiene exactamente un tipo máximo general (llamado su tipo principal ), que se considera el tipo canónico de esa expresión. En términos de polimorfismo de subtipo "basado en restricciones" (ver arriba), el tipo principal de una expresión es el subtipo único de cada tipo posible en el que se puede usar esa expresión. La presencia de tipeo principal en Haskell (no extendido) es lo que permite una inferencia de tipo completa (es decir, una inferencia de tipo exitosa para cada expresión, sin necesidad de anotaciones de tipo). Las extensiones que rompen la tipificación principal (de las cuales hay muchas) también rompen la integridad de la inferencia de tipos.

Llama de Ptharien
fuente
77
No lo use lcomo variable de una sola letra, ¡es MUY difícil distinguirlo 1!
recursion.ninja
55
Vale la pena señalar que, si bien tiene toda la razón de que Java tiene información sobre el tipo de tiempo de ejecución y Haskell no, puede usar la clase de tipo Typeable en Haskell para proporcionar algo que se comporta como información de tipo de tiempo de ejecución para muchos tipos (con PolyKinded más reciente clases en el camino, serán todos los tipos iirc), aunque creo que depende de la situación si realmente pasa cualquier tipo de información en tiempo de ejecución o no.
3
@DarkOtter Soy consciente Typeable, pero Haskell 2010 no lo tiene (¿tal vez Haskell 2014 sí?).
Ptharien's Flame
55
¿Qué pasa con los tipos de suma (cerrada)? Son uno de los mecanismos más importantes para codificar restricciones.
tibbe
3
Nulabilidad? Solidez (sin covarianza sillinses)? ¿Tipos de suma cerrada / coincidencias de patrones? Esta respuesta es demasiado estrecha
Peaker
32

El sistema de tipos de Java carece de un polimorfismo de tipo superior; El sistema de tipos de Haskell lo tiene.

En otras palabras: en Java, los constructores de tipos pueden abstraer sobre los tipos, pero no sobre los constructores de tipos, mientras que en Haskell, los constructores de tipos pueden abstraer sobre los constructores de tipos y los tipos.

En inglés: en Java, un genérico no puede tomar otro tipo genérico y parametrizarlo,

public void <Foo> nonsense(Foo<Integer> i, Foo<String> j)

mientras que en Haskell esto es bastante fácil

higherKinded :: Functor f => f Int -> f String
higherKinded = fmap show
Jörg W Mittag
fuente
28
¿Te importaría hacerlo de nuevo por nosotros, esta vez en inglés? : P
Mason Wheeler
8
@ Matt: A modo de ejemplo no puedo escribir esto en Java, pero puede escribir el equivalente en Haskell: <T<_> extends Collection> T<Integer> convertStringsToInts(T<string> strings). La idea aquí sería que si alguien lo llamara, convertStringsToInts<ArrayList>tomaría una lista de cadenas y devolvería una lista de enteros. Y si en su lugar lo usaran convertStringsToInts<LinkedList>, sería lo mismo con las listas vinculadas.
sepp2k
8
¿No es este polimorfismo de tipo superior, en lugar de rango 1 vs n?
Adam
8
@ JörgWMittag: Entiendo que el polimorfismo de rango superior se refiere a dónde puedes poner foralltus tipos. En Haskell, un tipo a -> bes implícitamente forall a. forall b. a -> b. Con una extensión, puede hacer que estos forallmensajes sean explícitos y moverlos.
Tikhon Jelvis el
8
@ Adam tiene derecho: un rango más alto y un tipo más alto son totalmente diferentes. GHC también puede hacer tipos mejor clasificados (es decir, para todos los tipos) con alguna extensión de idioma. Java no conoce los tipos de clase más alta ni de clase más alta.
Ingo
11

Para complementar las otras respuestas, el sistema de tipos de Haskell no tiene subtipos , mientras que los lenguajes orientados a objetos mecanografiados como Java.

En la teoría del lenguaje de programación , el subtipo (también polimorfismo de subtipo o polimorfismo de inclusión ) es una forma de polimorfismo de tipo en el que un subtipo es un tipo de datos que está relacionado con otro tipo de datos (el supertipo ) por alguna noción de sustituibilidad , lo que significa que los elementos del programa, generalmente subrutinas o funciones, escritas para operar en elementos del supertipo también pueden operar en elementos del subtipo. Si S es un subtipo de T, la relación de subtipo a menudo se escribe S <: T, lo que significa que cualquier término de tipo S se puede usar de forma segura en un contexto dondeSe espera un término de tipo T. La semántica precisa del subtipo depende crucialmente de los detalles de lo que "se usa con seguridad en un contexto donde" significa en un lenguaje de programación dado. El sistema de tipos de un lenguaje de programación define esencialmente su propia relación de subtipo, que bien puede ser trivial.

Debido a la relación de subtipo, un término puede pertenecer a más de un tipo. El subtipo es, por lo tanto, una forma de polimorfismo tipo. En la programación orientada a objetos, el término 'polimorfismo' se usa comúnmente para referirse únicamente a este polimorfismo de subtipo , mientras que las técnicas de polimorfismo paramétrico se considerarían programación genérica ...

Petr Pudlák
fuente
44
Aunque eso no significa que no tengas polimorfismo ad-hoc. Lo haces, solo en una forma diferente (clases de tipo en lugar de polimorfismo de subtipo).
3
¡Subclasificar no es subtipar!
Frank Shearar
8

Una cosa que nadie ha mencionado hasta ahora es la inferencia de tipos: un compilador de Haskell generalmente puede inferir el tipo de expresiones, pero debe decirle al compilador de Java sus tipos en detalle. Estrictamente, esta es una característica del compilador, pero el diseño del lenguaje y el sistema de tipos determina si la inferencia de tipos es factible. En particular, la inferencia de tipos interactúa mal con el polimorfismo de subtipo de Java y la sobrecarga ad hoc. En contraste, los diseñadores de Haskell se esfuerzan por no introducir características que afecten la inferencia de tipos.

Otra cosa que la gente parece no haber mencionado hasta ahora son los tipos de datos algebraicos. Es decir, la capacidad de construir tipos a partir de sumas ('o') y productos ('y') de otros tipos. Las clases Java hacen productos (campo a y campo b, por ejemplo) bien. Pero en realidad no hacen sumas (campo a o campo b, por ejemplo). Scala tiene que codificar esto como clases de casos múltiples, que no es lo mismo. Y aunque funciona para Scala, es un poco exagerado decir que Java lo tiene.

Haskell también puede construir tipos de funciones utilizando el constructor de funciones, ->. Si bien los métodos de Java tienen firmas de tipo, no puede combinarlos.

El sistema de tipos de Java permite un tipo de modularidad que Haskell no tiene. Pasará un tiempo antes de que haya un OSGi para Haskell.

GarethR
fuente
1
@MattFenwick, modifiqué el tercer párrafo en función de sus comentarios. Los dos sistemas de tipo tratan las funciones de manera muy diferente.
GarethR
No llamaría a los ADT una característica del sistema de tipos. Puede emularlos completamente (aunque sea torpemente) con envoltorios OO.
Leftaroundabout
@leftaroundabout Creo que esto es discutible. Por ejemplo, podría haber cosas que son nativas de un sistema de tipos de un idioma, pero podrían implementarse con patrones de diseño en otro. Obviamente, la forma del patrón de diseño, en comparación con una nativa, es una solución alternativa. La solución alternativa debido a un sistema de tipo más débil.
Hola Angel
La respuesta elegida mencionaba 'inferencia de tipo completa' en la sección 'Escritura principal'. Java puede emular sumas con subtipos e información de tipo de tiempo de ejecución, pero como usted dice, no es lo mismo, ya que la suma no es un atributo holístico del sistema de tipos.
Shelby Moore III