O sistema de tipos de Haskell é formalmente equivalente ao do Java? [fechadas]

66

Eu percebo que algumas coisas são mais fáceis / difíceis em um idioma do que em outro, mas estou interessado apenas em recursos relacionados ao tipo que são possíveis em um e impossíveis / irrelevantes no outro. Para torná-lo mais específico, vamos ignorar as extensões do tipo Haskell, já que há tantos por aí que fazem todos os tipos de coisas legais / legais.

    
por GlenPeterson 08.10.2012 / 17:50
fonte

4 respostas

63

("Java", como usado aqui, é definido como padrão Java SE 7 ; "Haskell", como usado aqui, é definido como padrão Haskell 2010 .

Coisas que o sistema de tipos do Java tem, mas as do Haskell não:

  • polimorfismo de subtipo nominal
  • informações do tipo em tempo de execução parcial

Coisas que o sistema de tipos de Haskell tem, mas que o Java não possui:

  • polimorfismo ad-hoc limitado
    • dá origem ao polimorfismo de subtipo "baseado em restrição"
  • polimorfismo paramétrico de maior qualidade
  • digitação principal

EDITAR:

Exemplos de cada um dos pontos listados acima:

Exclusivo para Java (em comparação com o Haskell)

Polimorfismo de subtipo nominal

/* 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 */

Informações do tipo de tempo de execução 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 para o Haskell (em comparação com o Java)

Polimorfismo ad-hoc limitado

-- 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 "baseado em restrições" (baseado em polimorfismo ad-hoc limitado)

-- 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 maior qualidade

-- 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

Digitação principal

Este é difícil de dar um exemplo direto, mas significa que toda expressão tem exatamente um tipo maximalmente geral (chamado de tipo principal ), que é considerado o tipo canônico daquela expressão. Em termos de polimorfismo de subtipo "baseado em restrição" (ver acima), o tipo principal de uma expressão é o subtipo único de cada tipo possível para o qual essa expressão pode ser usada. A presença de digitação principal (não estendida) Haskell é o que permite a inferência de tipos completa (isto é, inferência de tipo bem-sucedida para cada expressão, sem qualquer tipo de anotação necessária). Extensões que quebram a digitação principal (que são muitas) também quebram a integridade da inferência de tipos.

    
por 09.10.2012 / 06:37
fonte
32

O sistema de tipos de Java não possui um polimorfismo mais elevado; O sistema de tipos de Haskell tem isso.

Em outras palavras: em Java, os construtores de tipo podem abstrair os tipos, mas não os construtores de tipos, enquanto no Haskell, os construtores de tipos podem abstrair os construtores de tipos e os tipos.

Em inglês: em Java, um genérico não pode receber outro tipo genérico e parametrizá-lo,

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

enquanto em Haskell isso é muito fácil

higherKinded :: Functor f => f Int -> f String
higherKinded = fmap show
    
por 08.10.2012 / 18:30
fonte
11

Para complementar as outras respostas, o sistema de tipos de Haskell não possui subtipagem , enquanto as linguagens orientadas a objeto são digitadas como Java .

In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, meaning that program elements, typically subroutines or functions, written to operate on elements of the supertype can also operate on elements of the subtype. If S is a subtype of T, the subtyping relation is often written S <: T, to mean that any term of type S can be safely used in a context where a term of type T is expected. The precise semantics of subtyping crucially depends on the particulars of what "safely used in a context where" means in a given programming language. The type system of a programming language essentially defines its own subtyping relation, which may well be trivial.

Due to the subtyping relation, a term may belong to more than one type. Subtyping is therefore a form of type polymorphism. In object-oriented programming the term 'polymorphism' is commonly used to refer solely to this subtype polymorphism, while the techniques of parametric polymorphism would be considered generic programming...

    
por 08.10.2012 / 23:20
fonte
8

Uma coisa que ninguém mencionou até agora é a inferência de tipos: um compilador Haskell geralmente pode inferir o tipo de expressões, mas você precisa dizer ao compilador Java seus tipos em detalhes. Estritamente, este é um recurso do compilador, mas o design do sistema de idioma e tipo determina se a inferência de tipos é viável. Em particular, a inferência de tipos interage mal com o polimorfismo de subtipo de Java e a sobrecarga ad hoc. Em contraste, os designers do Haskell se esforçam para não introduzir recursos que impactam a inferência de tipos.

Outra coisa que as pessoas não parecem ter mencionado até agora são os tipos de dados algébricos. Ou seja, a capacidade de construir tipos de somas ('ou') e produtos ('e') de outros tipos. Classes Java fazem produtos (campo ae campo b, digamos) bem. Mas eles não fazem realmente somas (campo um campo OR b, digamos). O Scala tem que codificar isso como várias classes de casos, o que não é exatamente o mesmo. E, embora funcione para o Scala, é um pouco difícil dizer que o Java o possui.

Haskell também pode construir tipos de função usando o construtor de função, - & gt ;. Embora os métodos do Java possuam assinaturas de tipos, você não pode combiná-los.

O sistema de tipos do Java permite um tipo de modularidade que o Haskell não possui. Vai demorar um pouco até que haja um OSGi para Haskell.

    
por 30.09.2013 / 20:43
fonte