Pourquoi Bounded n'est-il pas une sous-classe d'Enum à Haskell

Il semble que toute instance Bounded devrait avoir une implémentation saine d'Enum. Je ne peux pas personnellement penser à un contre-exemple, bien que si quelqu'un en trouve un qui n'est pas pathologique, je comprendrai pourquoi ce n'est pas le cas.

En faisant :isur les deux classes de caractères, il semble que la seule exception actuellement dans la bibliothèque standard soit pour les tuples, qui sont délimités mais pas les énumérations. Cependant, tout tuple Bounded doit également être énumérable de manière sensée, en incrémentant simplement le dernier élément, puis en bouclant lorsqu'il atteint maxBound.

Ce changement impliquerait probablement également l'ajout predBet / nextBou quelque chose comme ça à Bounded pour un moyen sûr / en boucle de parcourir les valeurs Enum. Dans ce cas, toEnum 0 :: (...)serait égal à(toEnum 0, toEnum 0, ...) :: (...)

haskell typeclass point-virgule
la source

Je ne peux pas vraiment répondre à cette question avec autorité, mais considérez la plage de tous les nombres réels entre 0 et 1. Il a des limites inférieures et supérieures claires mais il a d'innombrables membres infinis.

Doval

@Doval c'est un bon point. Cependant, la même chose pourrait être dite à propos de tous les nombres réels en général (membres infiniment infinis), mais Double/ Floatet tous les types similaires implémentent de Enumtoute façon, ils font juste succ = (+ 1)et fromEnum = truncate. La façon dont Haskell a du sens d'un point de vue pratique, sinon [0, 0,5 ..] et similaire ne fonctionnerait pas, il semble donc que Haskell ne se soucie pas de la comptabilité en ce qui concerne les énumérations.

point

Je ne savais pas que succest (+1). C'est étrange, car Doubleet Floatn'ont pas une précision infinie et sont donc énumérables - succaurait pu être défini comme +1 ULP .

Doval

@Doval Je pense que la raison en est que l'équipe centrale de Haskell voulait que [1 ..] signifie la même chose avec Doubles que cela signifie avec Ints.

point

Les doubles et les flottants @semicolon ne sont pas des nombres réels (par exemple, ne peuvent pas stocker PI dans un double sans perdre une certaine précision), ils sont donc énumérables

jk.

Réponses:

Un exemple pratique que j'aime vient du monde des langages de programmation: l'ensemble des types dans un système OO est borné et discret mais non énumérable, et partiellement ordonné mais pas totalement ordonné.

L'ordre partiel en question est la relation de sous-typage <:. La borne supérieure serait alors le type supérieur (dont C # appelle objectet Scala appelle Any), et la borne inférieure serait le type inférieur (Scala Nothing; C # / Java n'ont pas d'équivalent pour parler).

Cependant, il n'existe aucun moyen d'énumérer tous les types dans le système de types, vous ne pouvez donc pas écrire un instance Enum Type. Cela devrait être clair: les utilisateurs peuvent écrire leurs propres types, il n'y a donc aucun moyen de savoir ce qu'ils seront à l'avance. Vous pouvez énumérer tous les types dans un programme donné, mais pas dans l'ensemble du système.

De même, (selon une certaine définition raisonnable du sous-typage), <:est réflexif, transitif et antisymétrique mais pas total . Il existe des paires de types qui ne sont pas liées par <:. ( Catet Dogsont tous deux des sous-types de Animal, mais aucun n'est un sous-type de l'autre.)

Supposons que nous écrivons un compilateur pour un langage OO simple. Voici la représentation des types dans notre système:

data Type = Bottom | Class { name :: String, parent :: Type } | Top

Et la définition de la relation de sous-typage:

(<:) :: Type -> Type -> Bool
Bottom <: _ = True
Class _ _ <: Bottom = False
Class n t <: s@(Class m _)
    | n == m = True  -- you can't have different classes with the same name in this hypothetical language
    | otherwise = t <: s  -- try to find s in the parents of this class
Class _ _ <: Top = True
Top <: Top = True
Top <: _ = False

Cela nous donne également une relation de supertypage.

(>:) :: Type -> Type -> Bool
t >: s = s <: t

Vous pouvez également trouver la borne supérieure la moins haute de deux types,

lub :: Type -> Type -> Type
lub Bottom s = s
lub t Bottom = t
lub t@(Class _ p) s@(Class _ q) =
    | t >: s = t
    | t <: s = s
    | p >: s = p
    | t <: q = q
    | otherwise = lub p q
lub Top _ = Top
lub _ Top = Top

Exercice: montrez que Typeforme un poset complet borné de deux manières, sous <:et sous >:.

Benjamin Hodgson
la source

Super merci! Cela répond complètement à ma question et répond également à ma question de suivi sur Ord. Eq aurait-il des problèmes similaires? Où un type non équitable peut avoir un maxBound ou un minBound. Dans ce cas, Cat == Dog devrait-il simplement retourner false, car ce sont des classes différentes, ou serait-il indécidable en raison de la position de l'arbre qui ne place ni au-dessus ni en dessous de l'autre?

point

Un ordre implique une égalité - il suffit de définir x == y = x <= y && y <= x. Si je concevais une Posetclasse, j'en aurais class Eq a => Poset a. Un rapide Google confirme que d' autres personnes ont eu la même idée .

Benjamin Hodgson

Désolé, ma question était ambiguë. Ce que je voulais dire, c'est si Bounded impliquait Eq même si cela n'implique pas Ord.

point

@semicolon Encore une fois, il n'y a aucune relation entre les deux classes. Considérez data Bound a = Min | Val a | Maxqui augmente un type aavec +∞et les -∞éléments. Par construction, Bound aon peut toujours en faire une instance, Boundedmais ce ne serait équitable que si le type sous-jacent aest

Benjamin Hodgson

bien assez juste. Je suppose qu'un exemple pourrait être des fonctions qui prennent et retournent des valeurs de type Double, où const (1/0)est maxBoundet const (negate 1/0)est minBoundmais \x -> 1 - xet qui \x -> x - 1sont incomparables.

point

C'est parce que les opérations sont indépendantes, donc les lier avec une relation de sous-classe ne vous rapporte rien. Supposons que vous vouliez créer un type personnalisé qui soit implémenté Bounded, peut-être Doublescontraint entre un max et un min, mais que vous n'aviez besoin d'aucune des Enumopérations. Si Boundedc'était une sous-classe, il faudrait Enumquand même implémenter toutes les fonctions, juste pour la faire compiler.

Peu importe s'il existe une implémentation raisonnable pour Enum, ou tout autre nombre de classes de caractères. Si vous n'en avez pas réellement besoin, vous ne devriez pas être obligé de l'implémenter.

Comparez cela avec, disons, Ordet Eq. Là, les Ordopérations dépendent de Eqcelles-ci, il est donc logique d'exiger la sous-classe pour éviter les doublons et garantir la cohérence.

Karl Bielefeldt
la source

Dans ces cas, cela fait partie de la définition. Toutes les monades sont également des applications et des foncteurs par définition, vous ne pouvez donc pas remplir le "contrat" de la monade sans remplir les autres. Je ne connais pas suffisamment les mathématiques pour savoir s'il s'agit d'une relation fondamentale ou d'une définition imposée, mais de toute façon, nous sommes coincés avec elle maintenant.

Karl Bielefeldt

@semicolon La documentation pourBounded indique que "Ord n'est pas une superclasse de Bounded car les types qui ne sont pas totalement ordonnés peuvent également avoir des limites supérieures et inférieures."

Benjamin Hodgson

@BenjaminHodgson Je n'ai même pas pensé aux types partiellement ordonnés. +1 pour un exemple non pathologique et pour citer la documentation.

Doval

@semicolon Un exemple de commande partielle dans le monde des ordinateurs pourrait être le sous-typage dans les langues OO. Écrire <:pour est un sous-type de , ∀ T S. T <: S ∨ S <: Tne tient pas (par exemple, int !<: bool ∧ bool !<: int). Vous rencontreriez probablement cela si vous écriviez un compilateur.

Benjamin Hodgson

@BenjaminHodgson ah ok. Ainsi, par exemple, si A est une superclasse de B et C, et D est une sous-classe de B et C, alors B et C sont incomparables mais A et D sont max / min?

point