Étant donné le type existentiel
T = ∃X.{op₁:X, op₂:X→boolean}
et cette interface Java générique:
interface T<X> {
X op₁();
boolean op₂(X something);
}
Quelles sont les différences fondamentales entre le type existentiel et l'interface Java?
Évidemment, il existe des différences syntaxiques et l'orientation objet de Java (qui comprend également des détails tels que les this
paramètres cachés , etc.). Je ne m'intéresse pas tant à celles-ci qu'aux différences conceptuelles et sémantiques - bien que si quelqu'un souhaite faire la lumière sur certains points plus fins (tels que la différence de notation entre T
vs T<X>
), cela serait également apprécié.
java
interfaces
type-systems
stakx
la source
la source
Réponses:
Hmm ... Cette définition ressemble beaucoup à un échantillon de haskell que j'ai vu il y a longtemps.
Lorsque le constructeur
X
est appliqué, becomes devient en fait ∃. Notez que lorsque vous sortez,value
vous ne connaissez pas le type et avez un ensemble d'opérations vide dessus. Mais comme ilviewValue
est un peu cohérent,value
il peut lui être appliqué.Je suppose que la principale différence de Java que
interface
vous avez proposée est le fait que vous devez connaître le type intermédiaire pour passer le résultat deop₁
àop₂
. C'est-à-dire que le système approprié pour le type existentiel doit sélectionner le bon type qui est garanti d'exister par condition. -À- dire , vous devriez être en mesure d'écrire la fonction de type:∀X. X→(X→boolean)→T
. Dans l'exemple précédent, cette fonction est leX
constructeur utilisé dansX 3 show
(show
est la fonction qui prend l'argument de tout type qui implémenteShow
et renvoieString
)Mise à jour: je viens de relire votre question et je pense que j'ai une bonne construction pour Java:
Vous avez raison de mentionner
this
- c'est en fait votre op₁.Donc je suppose que j'ai compris maintenant que les langages OOP classiques (Java, C #, C ++ etc) implémentent toujours un type existentiel avec une valeur unique
this
et une fonction dessus appelée "méthodes" qui implicitement appelées avec cette valeur :)PS Désolé, je ne suis pas très familier avec Java, mais j'espère que vous avez l'idée.
la source
La seule différence est que l'interface Java signifie réellement quelque chose pour le compilateur Java.
Le type existentiel est la définition formelle d'un type, non spécifique à n'importe quelle langue. Les informaticiens utilisent ce type de définition pour prouver les choses sur le type et sur les langages qui le mettent en œuvre. L'interface Java est l'une des implémentations Java du type défini formellement.
la source
Les 2 types présentés sont très différents l'un de l'autre. La définition d'interface que vous avez écrite est de type universel (les génériques Java en général appartiennent à cette catégorie).
Un type existentiel cache un type dans son implémentation au consommateur. Intuitivement, pour que X soit existentiel dans T, l'identité de X ne peut être connue d'aucun consommateur; il suffit de connaître l'ensemble des opérations prévues à la définition. Il existe un type T pour certains types X.
En revanche, un type universel définit des opérations applicables à tous les types, parmi lesquelles le consommateur est libre de choisir. Le type d'interface T est exactement cela. X est instancié par le consommateur, qui saura exactement de quel type X il s'agit. Il existe un type T pour chaque type X dans l'univers.
Les existentiels ne sont pas réellement présents dans Java en tant que construction de langage, sauf dans le cas limité des caractères génériques (
List<?>
). Mais oui, ils peuvent être émulés avec des interfaces. Le problème devient alors plus de conception.Comme on l'a souligné, dans un cadre orienté objet, les existentiels deviennent difficiles à implémenter car la façon dont vous codez généralement les informations de type de X (ce que vous pouvez en faire) est d'avoir des fonctions membres dans un type d'interface que X implémente. En bref, les interfaces peuvent acheter certaines capacités d'abstraction de type, mais nécessitent l'élimination de l'existentiel dans une certaine mesure.
la source