Le système de types de Haskell est-il formellement équivalent à celui de Java? [fermé]

66

Je réalise que certaines choses sont plus faciles / plus difficiles dans une langue que dans l'autre, mais je ne m'intéresse qu'aux fonctionnalités liées au type qui sont possibles dans l'une et impossibles / non pertinentes dans l'autre. Pour le rendre plus spécifique, ignorons les extensions de type Haskell car il y en a tellement qui font toutes sortes de choses folles / cools.

GlenPeterson
la source
4
Je suis moi aussi curieux d’entendre les théoriciens de la longue catégorie répondre à cette question; Bien que je doute de le comprendre particulièrement, je suis toujours intéressé par un détail de cela. Ce que j’ai lu, c’est que le système de types HM permet au compilateur d’en savoir beaucoup sur ce que fait votre code. C’est pourquoi il est capable de déduire autant de types que de donner autant de garanties sur le comportement. Mais ce n’est que mon instinct et je suis sûr qu’il ya d’autres choses que je ne connais absolument pas.
Jimmy Hoffa
1
C'est une excellente question - il est temps de tweeter sur Twitter pour le grand débat Haskell / JVM!
Martijn Verburg
6
@ m3th0dman: Scala supporte exactement le même support que Java pour les fonctions d'ordre supérieur. En Scala, les fonctions de première classe sont simplement représentées sous la forme d'instances de classes abstraites avec une seule méthode abstraite, tout comme Java. Bien sûr, Scala a un sucre syntaxique pour définir ces fonctions, et il possède une riche bibliothèque standard de types de fonctions prédéfinis et de méthodes qui acceptent les fonctions, mais du point de vue du système de types , de quoi traite cette question, il n'y a pas de différence . Donc, si Scala peut le faire, Java aussi, et il existe en fait des bibliothèques de FP inspirées de Haskell pour Java.
Jörg W Mittag
2
@ m3th0dman: Ce n'est pas de quoi parle cette question.
Phil
7
@ m3th0dman Ce sont des types parfaitement ordinaires. Les listes n’ont rien de spécial, à part quelques subtilités synactiques. Vous pouvez facilement définir votre propre type de données algébrique équivalent au type de liste intégré, à l'exception de la syntaxe littérale et des noms des constructeurs.
sepp2k

Réponses:

63

("Java", tel qu'utilisé ici, est défini en tant que norme Java SE 7 ; "Haskell", tel qu'utilisé ici, est défini en tant que norme Haskell 2010. )

Ce que le système de types de Java a mais que Haskell n'a pas:

  • polymorphisme nominal de sous-type
  • informations de type d'exécution partielle

Choses que le système de types de Haskell a mais que celles de Java ne:

  • polymorphisme ad-hoc lié
    • donne lieu à un polymorphisme de sous-type "basé sur des contraintes"
  • polymorphisme paramétrique de type supérieur
  • dactylographie principale

MODIFIER:

Exemples de chacun des points énumérés ci-dessus:

Unique à Java (par rapport à Haskell)

Polymorphisme nominal de sous-type

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

Informations de type d'exécution partielle

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

Unique à Haskell (par rapport à Java)

Polymorphisme ad hoc limité

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

Polymorphisme de sous-type "basé sur des contraintes" (basé sur un polymorphisme ad-hoc lié)

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

Polymorphisme paramétrique de type élevé

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

Dactylographie principale

Il est difficile de donner un exemple direct avec celui-ci, mais cela signifie que chaque expression a exactement un type général maximum (appelé son type principal ), qui est considéré comme le type canonique de cette expression. En termes de polymorphisme de sous-type "basé sur la contrainte" (voir ci-dessus), le type principal d'une expression est le sous-type unique de chaque type possible dans lequel cette expression peut être utilisée. La présence d'un typage principal dans Haskell (non étendu) est ce qui permet une inférence de type complète (c'est-à-dire une inférence de type réussie pour chaque expression, sans aucune annotation de type nécessaire). Les extensions qui rompent le typage principal (il en existe beaucoup) cassent également la complétude de l'inférence de type.

Flamme de Ptharien
la source
7
Ne pas utiliser lcomme une seule lettre variable, il est TRÈS difficile de distinguer 1!
recursion.ninja
5
Il peut être intéressant de noter que bien que vous ayez absolument raison que Java contienne des informations de type à l’exécution, contrairement à Haskell, vous pouvez utiliser la classe de types Typeable dans Haskell pour fournir quelque chose qui se comporte comme des informations de type d’exécution pour de nombreux types (avec les nouvelles versions de PolyKinded classes sur le chemin, ce sera tous les types iirc), bien que je pense que cela dépend de la situation si elle passe réellement toute information de type à l’exécution ou non.
3
Je suis conscient de @DarkOtter Typeable, mais Haskell 2010 ne l'a pas (peut-être que Haskell 2014 l'aura?).
La flamme de Ptharien le
5
Qu'en est-il des types de somme (fermés)? Ils sont l’un des mécanismes les plus importants pour les contraintes de codage.
Tibbe
3
Nullabilité? La solidité (pas de sillinses de covariance)? Somme fermée types / modèles correspond? Cette réponse est beaucoup trop étroite
Peaker
32

Le système de types de Java manque de polymorphisme plus élevé. Le système de types de Haskell l'a.

En d'autres termes: en Java, les constructeurs de types peuvent abstraire sur les types, mais pas sur les constructeurs de types, alors qu'en Haskell, les constructeurs de types peuvent abstraire sur les constructeurs de types ainsi que sur les types.

En anglais: en Java, un générique ne peut pas prendre un autre type générique et le paramétrer,

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

alors que dans Haskell c'est assez facile

higherKinded :: Functor f => f Int -> f String
higherKinded = fmap show
Jörg W Mittag
la source
28
Cela vous dérange-t-il à nouveau, en anglais cette fois? : P
Mason Wheeler
8
@ Matt: À titre d'exemple je ne peux pas écrire ce en Java, mais je peux écrire l'équivalent en Haskell: <T<_> extends Collection> T<Integer> convertStringsToInts(T<string> strings). L'idée ici serait que si quelqu'un l'appelait comme convertStringsToInts<ArrayList>cela prendrait un arrayliste de chaînes et renverrait un arrayliste d'entiers. Et s'ils utilisaient à la place convertStringsToInts<LinkedList>, ce serait la même chose avec les listes chaînées.
sepp2k
8
Ce polymorphisme de type supérieur n’est-il pas plutôt que rang 1 vs n?
Adam
8
@ JörgWMittag: D'après ce que je comprends, le polymorphisme de rang supérieur concerne les endroits où vous pouvez placer le foralldans vos types. En Haskell, un type a -> best implicitement forall a. forall b. a -> b. Avec une extension, vous pouvez forallles expliciter et les déplacer.
Tikhon Jelvis
8
@Adam est exact: les grades les plus élevés et les plus gentils sont totalement différents. GHC peut également créer des types de classement supérieur (c.-à-d. Tous les types) avec une extension de langue. Java ne connaît ni les types mieux classés ni les types mieux classés.
Ingo
11

Pour compléter les autres réponses, le système de types de Haskell ne comporte pas de sous - typage , contrairement aux langages orientés objet typés, comme le fait Java.

En théorie du langage de programmation , le sous - type (également le polymorphisme de sous-type ou le polymorphisme d' inclusion ) est une forme de polymorphisme de type dans laquelle un sous - type est un type de données lié à un autre type de données (le supertype ) par une notion de substituabilité , ce qui signifie que les éléments de programme, généralement des sous-programmes ou des fonctions, écrites pour agir sur des éléments du supertype, peuvent également agir sur des éléments du sous-type. Si S est un sous-type de T, la relation de sous-typage est souvent écrite S <: T, pour signifier que tout terme de type S peut être utilisé en toute sécurité dans un contexte oùun terme de type T est attendu. La sémantique précise du sous-typage dépend de manière cruciale de ce que "est utilisé en toute sécurité dans un contexte où" signifie dans un langage de programmation donné. Le système de types d'un langage de programmation définit essentiellement sa propre relation de sous-typage, qui peut être triviale.

En raison de la relation de sous-typage, un terme peut appartenir à plus d'un type. Le sous-typage est donc une forme de polymorphisme de type. Dans la programmation orientée objet, le terme «polymorphisme» est couramment utilisé pour désigner uniquement ce polymorphisme de sous - type , alors que les techniques de polymorphisme paramétrique seraient considérées comme une programmation générique ...

Petr Pudlák
la source
4
Bien que cela ne signifie pas que vous n’obtenez pas de polymorphisme ad hoc. Vous faites, juste sous une forme différente (classes de type au lieu de polymorphisme de sous-type).
3
Le sous-classement n'est pas le sous-typage!
Frank Shearar
8

L'inférence de type est une chose que personne n'a encore mentionnée: un compilateur Haskell peut généralement déduire le type d'expressions, mais vous devez indiquer vos types au compilateur Java en détail. Strictement, il s’agit d’une caractéristique du compilateur, mais la conception du langage et du système de types détermine si l’inférence de type est réalisable. En particulier, l'inférence de type interagit mal avec le polymorphisme de sous-type et la surcharge ad hoc de Java. En revanche, les concepteurs de Haskell s'efforcent de ne pas introduire de fonctionnalités ayant un impact sur l'inférence de type.

Une autre chose que les gens ne semblent pas avoir mentionnée jusqu’à présent concerne les types de données algébriques. C'est-à-dire la capacité de construire des types à partir de sommes ('ou') et de produits ('et') d'autres types. Les classes Java font des produits (champ a et champ b, disons) bien. Mais ils ne font pas vraiment de sommes (champ a OU ou champ b, disons). Scala doit l'encoder sous forme de plusieurs classes de cas, ce qui n'est pas tout à fait la même chose. Et bien que cela fonctionne pour Scala, il est un peu exagéré de dire que Java l’a.

Haskell peut également construire des types de fonction en utilisant le constructeur de fonction, ->. Bien que les méthodes de Java aient des signatures de type, vous ne pouvez pas les combiner.

Le système de types de Java permet un type de modularité que Haskell n'a pas. Il faudra un certain temps avant qu’il n’y ait un OSGi pour Haskell.

GarethR
la source
1
@ MattFenwick, j'ai modifié le 3ème paragraphe en fonction de vos commentaires. Les deux systèmes de types traitent les fonctions très différemment.
GarethR
Je n'appellerais pas ADT une fonctionnalité du système de types. Vous pouvez pleinement (si maladroitement) les imiter avec des wrappers OO.
gauche du
@leftaroundabout Je pense que c'est sans doute. Par exemple, certains éléments peuvent être natifs d’un système de types d’un langage, mais être implémentés avec des modèles de conception dans un autre. Évidemment, la méthode de conception, comparée à une méthode native, est une solution de contournement. La solution de contournement due à un système de type plus faible.
Bonjour Angel
La réponse choisie mentionnait «inférence de type complète» dans la section «Typage principal». Java peut en quelque sorte émuler des sommes avec des sous-types et des informations de type à l'exécution, mais comme vous le dites, ce n'est pas la même chose, car la somme n'est pas un attribut holistique du système de types.
Shelby Moore III