Il sistema di tipo Haskell è formalmente equivalente a quello di Java? [chiuso]

66

Mi rendo conto che alcune cose sono più facili / più difficili in una lingua rispetto all'altra, ma mi interessano solo le funzionalità correlate al tipo che sono possibili in una e impossibili / irrilevanti nell'altra. Per renderlo più specifico, ignoriamo le estensioni di tipo Haskell poiché ce ne sono così tante che fanno tutti i tipi di cose pazzesche / interessanti.

    
posta GlenPeterson 08.10.2012 - 17:50
fonte

4 risposte

63

("Java", come usato qui, è definito come standard Java SE 7 ; "Haskell", come usato qui, è definito come standard Haskell 2010 .)

Cose che il sistema di tipi di Java ha ma che Haskell non ha:

  • polimorfismo del sottotipo nominale
  • informazioni sul tipo di runtime parziale

Cose che il sistema di tipi di Haskell ha ma che Java non ha:

  • polimorfismo ad-hoc limitato
    • dà origine al "polimorfismo di sottotipo" basato sui vincoli
  • polimorfismo parametrico di tipo superiore
  • tipizzazione principale

Modifica

Esempi di ciascuno dei punti sopra elencati:

Unico a Java (rispetto a Haskell)

Polimorfismo dei sottotipi nominali

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

Informazioni sul tipo di runtime parziale

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

Unico per Haskell (rispetto a Java)

Polimorfismo ad-hoc limitato

-- 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 del sottotipo "basato sui vincoli" (basato sul polimorfismo ad-hoc limitato)

-- 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 parametrico di tipo superiore

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

Digitazione principale

Questo è difficile da dare un esempio diretto di, ma significa che ogni espressione ha esattamente un tipo massimale generale (chiamato il suo tipo principale ), che è considerato il tipo canonico di quell'espressione. In termini di polimorfismo del sottotipo "basato su vincoli" (vedi sopra), il tipo principale di un'espressione è il sottotipo unico di ogni tipo possibile che l'espressione può essere utilizzata come. La presenza del principale digitando in Haskell (non ampliato) è ciò che consente l'inferenza completa del tipo (vale a dire, l'inferenza di tipo riuscita per ogni espressione, senza bisogno di annotazioni di tipo). Le estensioni che interrompono la tipizzazione principale (di cui ce ne sono molte) interrompono anche la completezza dell'inferenza di tipo.

    
risposta data 09.10.2012 - 06:37
fonte
32

Il sistema di tipi di Java non ha il polimorfismo di tipo più elevato; Il sistema di tipi di Haskell ce l'ha.

In altre parole: in Java, i costruttori di tipi possono astrarre su tipi, ma non su costruttori di tipi, mentre in Haskell, i costruttori di tipi possono astrarre su tipi di costruttori e tipi.

In inglese: in Java un generico non può prendere un altro tipo generico e parametrizzarlo,

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

mentre in Haskell questo è abbastanza facile

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

Per completare le altre risposte, il sistema di tipi di Haskell non ha sottotipo , mentre i linguaggi orientati agli oggetti scritti come Java fanno .

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

    
risposta data 08.10.2012 - 23:20
fonte
8

Una cosa che nessuno ha menzionato finora è l'inferenza del tipo: un compilatore Haskell di solito può inferire il tipo di espressioni, ma devi dire al compilatore Java i tuoi tipi in dettaglio. Rigorosamente, questa è una caratteristica del compilatore, ma il design del linguaggio e del sistema di tipi determina se l'inferenza di tipo è fattibile. In particolare, l'inferenza di tipo interagisce male con il polimorfismo del sottotipo di Java e l'overloading ad hoc. Al contrario, i progettisti di Haskell si sforzano di non introdurre funzionalità che influiscano sull'inferenza di tipo.

Un'altra cosa che le persone non sembrano aver menzionato finora sono i tipi di dati algebrici. Cioè, la capacità di costruire tipi da somme ('o') e prodotti ('e') di altri tipi. Le classi Java fanno i prodotti (campo a e campo b, diciamo) bene. Ma in realtà non fanno somme (campo a campo OR b, per esempio). Scala deve codificarlo come più case case, che non è esattamente la stessa cosa. E mentre funziona per Scala è un po 'difficile dire che Java ce l'ha.

Haskell può anche costruire tipi di funzione usando il costruttore di funzioni, - & gt ;. Mentre i metodi Java hanno le firme dei tipi, non puoi combinarle.

Il sistema di tipi di Java abilita un tipo di modularità che Haskell non ha. Ci vorrà un po 'prima che ci sia un OSGi per Haskell.

    
risposta data 30.09.2013 - 20:43
fonte

Leggi altre domande sui tag