IdentifiantMot de passe
Loading...
Mot de passe oublié ?Je m'inscris ! (gratuit)
Navigation

Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter

Haskell Discussion :

Liens entre classes Monad, Functor, etc.


Sujet :

Haskell

  1. #1
    Membre du Club Avatar de limestrael
    Profil pro
    Inscrit en
    Juin 2009
    Messages
    86
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Juin 2009
    Messages : 86
    Points : 57
    Points
    57
    Par défaut Liens entre classes Monad, Functor, etc.
    Une question que je me pose depuis un moment déjà :

    D'après ce que j'ai compris, toute Monad est un Applicative, de même que tout Applicative est un Functor, et tout Functor est une Arrow.
    Arrêtez-moi si je me trompe, mais si j'ai raison, dans ce cas est-ce que, lorsqu'on défini un type comme étant une instance de Monad, l'instanciation de Functor, Applicative et Arrow se fait automatiquement ?

    Pour la généralisation Monad => Functor, pour moi on peut faire :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    instance Monad m => Functor m where
        fmap f x = x >>= return . f
    De même, on peut généraliser les Applicatives aux functors avec:
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    instance Applicative f => Functor f where
        fmap f app = pure f <*> app
    Et pour finir, généraliser les Monads aux Applicatives :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    instance Monad m => Applicative m where
        pure x = return x
        f <*> x = f >>= (\fct -> x >>= return . fct)
    Pour la généralisation aux Arrows, là je sais pas, je ne les ai pas encore utilisées.

    Si cela est aussi simple, alors Haskell le fait-il automatiquement ?

  2. #2
    Expert éminent
    Avatar de Jedai
    Homme Profil pro
    Enseignant
    Inscrit en
    Avril 2003
    Messages
    6 245
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Côte d'Or (Bourgogne)

    Informations professionnelles :
    Activité : Enseignant

    Informations forums :
    Inscription : Avril 2003
    Messages : 6 245
    Points : 8 586
    Points
    8 586
    Par défaut
    Je dirais plutôt "tout Arrow est un Functor", pas l'inverse, en plus c'est faux semble-t-il.

    Haskell ne fait pas toutes ces instances automatiquement et il ne vérifie même pas si les instances existent, d'une part pour des raisons historiques (le report a été écrit à une période où Applicative n'existait pas, et on n'a pas pensé à mettre Functor en tant que classe parente de Monad) et d'autre part pour des raisons pratiques : les instances que tu viens d'écrire marcheraient, mais elle seraient plutôt inefficientes en général, et avoir à la fois une instance globale et des instances spécifiques nécessiterait d'activer par défaut une extension (OverlappingInstance) plutôt inélégante.

    Si le Prelude était réécrit aujourd'hui, Monad serait plutôt :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    class (Functor m, Applicative m) => Monad m where ...
    avec des implémentations par défaut, autrement dit on procèderait plutôt dans le sens inverse de ta proposition.

    Si tu veux un article clair sur ces typeclass et leur relations, je te recommande "The Typeclassopedia" dans Monad Reader n°13 (magazine que je te recommande chaudement en général).

    --
    Jedaï

    PS : GHC 6.12 saura dériver Functor, Foldable et Traversable automatiquement (GHC HEAD sait déjà le faire) avec une clause deriving.
    PPS : Par ailleurs il est fort possible que dans une réécriture de la classe Monad et des classes Functor et Applicative, on utilise les types families et les classes à plusieurs paramètres pour permettre de faire des monades pour Ord, Set et autres...

  3. #3
    Membre du Club Avatar de limestrael
    Profil pro
    Inscrit en
    Juin 2009
    Messages
    86
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Juin 2009
    Messages : 86
    Points : 57
    Points
    57
    Par défaut
    Citation Envoyé par Jedai Voir le message
    Je dirais plutôt "tout Arrow est un Functor", pas l'inverse, en plus c'est faux semble-t-il.
    Je croyais que les Arrows étaient la généralisation de tout ?

    les instances que tu viens d'écrire marcheraient, mais elle seraient plutôt inefficientes en général
    Pourquoi donc ? Elles décrivent pourtant correctement le fonctionnement des types. Par exemple, List est une Monad, et en définissant Functor à partir de Monad comme je l'ai fait on a exactement le comportement du Functor List tel que décrit actuellement en Haskell. Idem pour Maybe et IO. Je ne vois pas ce qui cloche.
    C'est logique : Si A implique B, alors A permet de faire tout ce que B permet de faire.

    et avoir à la fois une instance globale et des instances spécifiques nécessiterait d'activer par défaut une extension (OverlappingInstance) plutôt inélégante
    J'ai pas compris pourquoi non plus...

  4. #4
    Expert éminent
    Avatar de Jedai
    Homme Profil pro
    Enseignant
    Inscrit en
    Avril 2003
    Messages
    6 245
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Côte d'Or (Bourgogne)

    Informations professionnelles :
    Activité : Enseignant

    Informations forums :
    Inscription : Avril 2003
    Messages : 6 245
    Points : 8 586
    Points
    8 586
    Par défaut
    Citation Envoyé par limestrael Voir le message
    Je croyais que les Arrows étaient la généralisation de tout ?
    Oui, tout à fait (mais c'est un peu court comme description), ce qui signifie qu'elles ne sont pas grand chose (plus une chose est "générale", moins tu sais de choses dessus, moins tu peux les manipuler ). En fait lit la typeclassopedia, il y a un schéma des relations entre les classes de type dedans, où tu apprends que tout Arrow n'est pas un Functor, ni l'inverse, mais que tout ArrowApply (une spécialisation d'Arrow) est bien un Functor.

    Citation Envoyé par limestrael Voir le message
    Pourquoi donc ? Elles décrivent pourtant correctement le fonctionnement des types. Par exemple, List est une Monad, et en définissant Functor à partir de Monad comme je l'ai fait on a exactement le comportement du Functor List tel que décrit actuellement en Haskell. Idem pour Maybe et IO. Je ne vois pas ce qui cloche.
    C'est logique : Si A implique B, alors A permet de faire tout ce que B permet de faire.
    Ces instances sont correctes, je ne dis pas le contraire, mais au niveau des performances elles sont loin d'être optimale, et comme les Functors sont tout de même des composants essentiels et très fréquemment utilisés dans les projets Haskell sérieux, cette considération est loin d'être négligeable.
    Prenons l'exemple des listes, ton instance reviendrait à dire :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    fmap f xs = concatMap ((\x -> [x]) . f) xs
    Et il y a peu de chance que GHC optimise ceci en :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    fmap f xs = foldr (\x ys -> f x : ys) [] xs
    ou équivalent...
    (en fait ce n'est pas si improbable que ça dans ce cas précis, mais je pense que tu saisis mon argument en général )

    Citation Envoyé par limestrael Voir le message
    J'ai pas compris pourquoi non plus...
    Pourquoi quoi ? Pourquoi il faut activer OverlappingInstance pour avoir à la fois tes instances globales et des instances spécifiques ou pourquoi cette extension est inélégante si on peut l'éviter ?

    --
    Jedaï

  5. #5
    Membre du Club Avatar de limestrael
    Profil pro
    Inscrit en
    Juin 2009
    Messages
    86
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Juin 2009
    Messages : 86
    Points : 57
    Points
    57
    Par défaut
    Ces instances sont correctes, je ne dis pas le contraire, mais au niveau des performances elles sont loin d'être optimale, et comme les Functors sont tout de même des composants essentiels et très fréquemment utilisés dans les projets Haskell sérieux, cette considération est loin d'être négligeable.
    Prenons l'exemple des listes, ton instance reviendrait à dire :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    fmap f xs = concatMap ((\x -> [x]) . f) xs
    Et il y a peu de chance que GHC optimise ceci en :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    fmap f xs = foldr (\x ys -> f x : ys) [] xs
    ou équivalent...
    (en fait ce n'est pas si improbable que ça dans ce cas précis, mais je pense que tu saisis mon argument en général )
    Certes oui.

    Pourquoi quoi ? Pourquoi il faut activer OverlappingInstance pour avoir à la fois tes instances globales et des instances spécifiques ou pourquoi cette extension est inélégante si on peut l'éviter ?
    Les deux, mon capitaine !

  6. #6
    Expert éminent
    Avatar de Jedai
    Homme Profil pro
    Enseignant
    Inscrit en
    Avril 2003
    Messages
    6 245
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Côte d'Or (Bourgogne)

    Informations professionnelles :
    Activité : Enseignant

    Informations forums :
    Inscription : Avril 2003
    Messages : 6 245
    Points : 8 586
    Points
    8 586
    Par défaut
    Citation Envoyé par limestrael Voir le message
    Les deux, mon capitaine !
    Et bien l'extension est nécessaire parce que en Haskell 98 tu ne peux pas avoir deux instances valables pour un même type, or si tu voulais avoir une instance générale plus des spécifiques, tu serais dans cette situation. Et cette extension est inélégante à mon sens parce qu'elle introduit des ambiguïtés, par exemple tu ne peux plus être sûr que ton instance va être choisie si quelqu'un en introduit une plus spécifique à côté, tu dois également connaître toutes les instances qui matchent un type pour savoir laquelle s'applique, tu ne peux pas te contenter de t'arrêter à la première que tu rencontres (en général), etc... Je n'aime pas trop l'idée quoi. Mais il y a des usages intéressant de OverlappingInstance, dans ce cas particulier je ne suis pas sûr qu'on en ait vraiment besoin (on peut aller dans l'autre sens comme je l'ai montré, si on est prêt à faire fi de l'établi).

    --
    Jedaï

  7. #7
    Membre du Club Avatar de limestrael
    Profil pro
    Inscrit en
    Juin 2009
    Messages
    86
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Juin 2009
    Messages : 86
    Points : 57
    Points
    57
    Par défaut
    D'accord merci.
    Je me rappelle des OverlappingInstances, Real World Haskell les utilise assez tôt.

  8. #8
    Membre du Club Avatar de limestrael
    Profil pro
    Inscrit en
    Juin 2009
    Messages
    86
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Juin 2009
    Messages : 86
    Points : 57
    Points
    57
    Par défaut
    Citation Envoyé par Jedai Voir le message
    Ces instances sont correctes, je ne dis pas le contraire, mais au niveau des performances elles sont loin d'être optimale, et comme les Functors sont tout de même des composants essentiels et très fréquemment utilisés dans les projets Haskell sérieux, cette considération est loin d'être négligeable.
    J'en reviens à ces histoires de perfs : je viens de découvrir la fonction 'ap' des monades, qui s'utilise comme ceci :

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    a = return someFunc `ap` someMonad `ap` someMonad `ap` someMonad
    Je m'excuse, mais ça c'est EXACTEMENT le mode de fonctionnement des Applicatives !

    On peut donc déterminer les équivalences suivantes :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    pure == return
    ap == (<*>)
    fmap == liftM
    On passe donc d'une façon hypra simple des monades aux applicatifs ou aux foncteurs.

    Donc, quand tu dis
    Ces instances sont correctes, je ne dis pas le contraire, mais au niveau des performances elles sont loin d'être optimale, et comme les Functors sont tout de même des composants essentiels et très fréquemment utilisés dans les projets Haskell sérieux, cette considération est loin d'être négligeable.
    tu utiliseras de toutes façons ton implémentation de fmap quand tu utiliseras un liftM.

  9. #9
    Expert éminent
    Avatar de Jedai
    Homme Profil pro
    Enseignant
    Inscrit en
    Avril 2003
    Messages
    6 245
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Côte d'Or (Bourgogne)

    Informations professionnelles :
    Activité : Enseignant

    Informations forums :
    Inscription : Avril 2003
    Messages : 6 245
    Points : 8 586
    Points
    8 586
    Par défaut
    Citation Envoyé par limestrael Voir le message
    J'en reviens à ces histoires de perfs : je viens de découvrir la fonction 'ap' des monades, qui s'utilise comme ceci :

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    a = return someFunc `ap` someMonad `ap` someMonad `ap` someMonad
    Je m'excuse, mais ça c'est EXACTEMENT le mode de fonctionnement des Applicatives !
    Pas la peine de t'excuser, ap et (<*>) sont effectivement des synonymes au niveau du sens.

    Citation Envoyé par limestrael Voir le message
    On peut donc déterminer les équivalences suivantes :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    pure == return
    ap == (<*>)
    fmap == liftM
    On passe donc d'une façon hypra simple des monades aux applicatifs ou aux foncteurs.

    tu utiliseras de toutes façons ton implémentation de fmap quand tu utiliseras un liftM.
    Non, en fait... non.
    La définition de liftM est la suivante (liftM n'est pas une méthode de Monad, c'est une fonction ordinaire) :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    liftM :: (Monad m) => (a -> b) -> m a -> m b
    liftM f m = m >>= return . f
    Donc liftM marche pour toutes les monades, et il est synonyme de fmap au niveau du sens, mais fmap étant une méthode peut être bien plus optimisé que liftM, si tu définis fmap en fonction de liftM comme tu l'as proposé, tu perds cette opportunité d'optimisation (sauf à faire aussi des instances plus spécifiques et utiliser OverlappingInstances). Ma proposition était à l'inverse de définir :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    class (Functor a) => Applicative a where
      blabla :: ... 
      blabla = définition par défaut utilisant fmap
      ...
     
    class (Applicative m) => Monad m where
      return :: a -> m a
      return = pure
      ....
     
    liftM :: (Monad m) => (a -> b) -> m a -> m b
    liftM = fmap
    Dans ce sens, tu gagnes effectivement un peu de blabla (grâce aux définitions par défaut de méthodes, sans doute moins que ta proposition toutefois) mais tu ne sacrifies pas du tout d'opportunité d'optimisation. Et la hiérarchie des typeclasses traduit enfin les relations entre les objets.

    --
    Jedaï

  10. #10
    Membre du Club Avatar de limestrael
    Profil pro
    Inscrit en
    Juin 2009
    Messages
    86
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Juin 2009
    Messages : 86
    Points : 57
    Points
    57
    Par défaut
    Mouaip, au final c'est encore toi qui as raison.

    Oui, ta solution est effectivement logique, on ne devrait pouvoir définir un type comme étant une Monade que s'il est déjà un Functor et un Applicative, c'est dommage que Simon, Paul, Philip et les autres n'en aient pas décidé ainsi...

  11. #11
    Membre éprouvé
    Profil pro
    Inscrit en
    Avril 2007
    Messages
    832
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Avril 2007
    Messages : 832
    Points : 1 104
    Points
    1 104
    Par défaut
    Il me semble qu'à l'époque on ne connaissait pas encore Applicative.
    Si les restricted monads entrent dans Haskell', on pourra faire ce genre de choses.

    De toute façon, ce genre de problème se reposera toujours : dès qu'on étudie un peu en profondeur des abstractions, on trouve des abstractions intermédiaires un peu plus générales et on a envie de redéfinir l'abstraction initiale en terme de ces dernières. Tu devras donc toujours modifier ta bibliothèque standard si tu veux "suivre le mouvement", jusqu'au moment où tu auras exactement une typeclasse par jeu de constructeurs. Le mieux serait d'avoir du sous-typage structurel ("ça connaît map donc c'est un foncteur"), mais je crois que les type-classes de Haskell ne permettent pas de faire cela sans écrire toutes les relations à la main.

  12. #12
    Membre du Club Avatar de limestrael
    Profil pro
    Inscrit en
    Juin 2009
    Messages
    86
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Juin 2009
    Messages : 86
    Points : 57
    Points
    57
    Par défaut
    Citation Envoyé par bluestorm Voir le message
    Il me semble qu'à l'époque on ne connaissait pas encore Applicative.
    Si les restricted monads entrent dans Haskell', on pourra faire ce genre de choses.
    Oui, c'est vrai qu'il y a aussi l'argument historique (Monad est plus spécifique que Applicative mais elle est quand même la depuis plus longtemps)

    Le mieux serait d'avoir du sous-typage structurel ("ça connaît map donc c'est un foncteur")
    Ca ressemble à du duck-typing.

  13. #13
    Rédacteur/Modérateur

    Avatar de gorgonite
    Homme Profil pro
    Ingénieur d'études
    Inscrit en
    Décembre 2005
    Messages
    10 322
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 39
    Localisation : France

    Informations professionnelles :
    Activité : Ingénieur d'études
    Secteur : Transports

    Informations forums :
    Inscription : Décembre 2005
    Messages : 10 322
    Points : 18 679
    Points
    18 679
    Par défaut
    Citation Envoyé par limestrael Voir le message
    Ca ressemble à du duck-typing.
    le duck-typing est dynamique... en statique, on pourrait voir une ressemblance avec le typage des objets sous OCaml, ou la génération d'interface minimale à la compilation sur les templates C++
    Evitez les MP pour les questions techniques... il y a des forums
    Contributions sur DVP : Mes Tutos | Mon Blog

  14. #14
    Membre émérite
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    Juin 2007
    Messages
    1 704
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : Juin 2007
    Messages : 1 704
    Points : 2 990
    Points
    2 990
    Par défaut
    En Coq 8.2 on a les modules d'ordre supérieur (typage structurel) et les types-classes et les types dépendants. C'est le langage idéal pour modéliser ce genre de hiérarchie d'abstractions.
    Par contre ces systèmes ne sont pas aussi matures que leur équivalent OCaml (pas d'include et pas pas de modules récursifs) ou Haskell (les types-classes sont une nouveauté de Coq 8.2).

    Citation Envoyé par gorgonite
    en statique, on pourrait voir une ressemblance avec le typage des objets sous OCaml, ou la génération d'interface minimale à la compilation sur les templates C++
    Ça irait dans le sens de la demande des utilisateurs .
    En pratique les programmeurs Coq n'utilisent pas vraiment le système de modules parce que les modules ne sont pas des first-class-objects. Les modules d'ordre supérieur sont trop orientés vers la structuration des programmes, à mon avis un système d'enregistrements extensibles aurait eu davantage de succès.
    Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

  15. #15
    Membre éprouvé
    Profil pro
    Inscrit en
    Avril 2007
    Messages
    832
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Avril 2007
    Messages : 832
    Points : 1 104
    Points
    1 104
    Par défaut
    En Coq 8.2 on a les modules d'ordre supérieur (typage structurel) et les types-classes et les types dépendants. C'est le langage idéal pour modéliser ce genre de hiérarchie d'abstractions.
    Ça ne résoud pas tous les problèmes, loin de là. En particulier, si certaines bibliothèques utilisent des foncteurs et d'autres de types-classes, il n'est pas clair du tout de pouvoir les faire communiquer convenablement. Ça pose des problèmes de software engineering non triviaux, et à ma connaissance on n'a pas de résultats concluants à ce sujet.

    Pour ce qui est de la représentation des hiérarchies d'abstraction, il y a par contre déjà de la recherche faite, par exemple sur un mélange d'objets et de modules. Je pense au papier "Modules, Objets et Calcul Formel" [1] et plus généralement les travaux du projet Focal [2].

    [1] est très intéressant parce qu'il montre plusieurs étapes de conception, avec des modules, des classes puis un mélange des deux, et je pense que ça illustre bien les questions en jeu ici. Ça reste limité aux outils du langage OCaml mais je trouve leur résultat très satisfaisant

    [2] propose de se baser sur d'autres concepts de base que les objets, modules ou typeclasses (les "espèces"). Ça fait longtemps que j'ai regardé et je ne m'en souviens plus très bien, d'autant qu'ils ont revu intégralement leur logiciel une ou deux fois, mais ça reste intéressant.

    Pour moi les typeclasses sont basées sur une méthode de résolution implicite basée sur les noms des types, et ce n'est pas la bonne solution parce que :
    - elle ne présente pas assez les aspects de "programmation logique" de leur moteur interne de satisfaction des instances pour être suffisamment expressive (je ne prétends pas pouvoir faire mieux, mais il me semble évident que dans un modèle où tout est caché au programmeur, on est forcément limité par rapport à un modèle plus explicite, et cette limitation se fera sentir un jour ou l'autre)
    - elle ne représente pas bien le domaine du problème qui nous concerne ici, à savoir gérer des hiérarchies d'abstractions mathématiques; en effet, il ne peut y avoir qu'une instance par type de base, alors qu'un ensemble mathématique peut supporter de nombreuses structures différentes (par exemple les entiers naturels sont à la fois un monoide additif et multiplicatif); on peut contourner cette difficulté en donnant différents noms au même type pour le munir de différentes instances, mais je ressens ça (je peux me tromper) comme un bidouillage qui cache les vraies limites de la chose.

    L'implémentation Haskell a d'autres problèmes, comme le fait que les type classes vivent dans un namespace global, ce qui peut poser de sérieux problèmes de modularité, mais je vois ça comme un défaut de mise en place plutôt qu'un défaut fondamental.

    En clair je pense que les type classes ne sont certainement pas la "bonne solution" au problème des hiérarchies de structure. Elles ont beaucoup de succès parce qu'elles sont une partie de la solution tout en étant très agréable à utiliser (puisque très implicites), c'est un genre de "sweet spot" très intéressant mais ça n'est pas ce qu'on peut faire de mieux.

    En l'état, les modules sont trop pénibles à utiliser pour remplir le même rôle, mais j'ai le sentiment qu'ils sont plus proches de ce qu'on veut. Ça reste des domaines assez compliqués (on dirait pas mais des modules à la SML/OCaml ça demande des choix de design considérables), et il y a de la bonne recherche à ces sujets (modules, species, mixins..), que je ne connais malheureusement pas vraiment (cf. par exemple la recherche de Derek Dreyer, il a un papier "Modular Type Classes" que je n'ai pas lu mais qui semble pertinent).

  16. #16
    Membre émérite
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    Juin 2007
    Messages
    1 704
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : Juin 2007
    Messages : 1 704
    Points : 2 990
    Points
    2 990
    Par défaut
    Citation Envoyé par bluestorm
    Citation Envoyé par SpiceGuid
    En Coq 8.2 on a les modules d'ordre supérieur (typage structurel) et les types-classes et les types dépendants. C'est le langage idéal pour modéliser ce genre de hiérarchie d'abstractions.
    Ça ne résoud pas tous les problèmes, loin de là.
    Disons que c'est un cadre riche et agréable pour réfléchir à la question.
    Ceci dit je suis plutôt d'accord avec ton opinion sur les typeclass ainsi qu'avec la remarque de gorgonite selon laquelle la POO est en fait mieux appropriée.

    Citation Envoyé par bluestorm
    En l'état, les modules sont trop pénibles à utiliser pour remplir le même rôle, mais j'ai le sentiment qu'ils sont plus proches de ce qu'on veut
    Les modules Coq ne sont pas si pénibles.
    Coq a des facilités pour passer implicitement des arguments qui font que les modules sont bien moins verbeux qu'en OCaml.

    Par exemple avec le mécanisme de Section nombre d'arguments deviennent implicites :
    Code Coq : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    16
    17
    18
    19
    20
    21
    22
    23
    24
    25
    26
    27
    28
    29
    30
    31
    32
    33
    34
    35
    36
    37
    38
    39
    40
    41
     
    Module Operation.
     
      Section operations.
     
      Variable U : Set.
     
      Definition Operation := U -> U -> U.
     
      Variable Op : Operation.   (* law       *)
     
      Variable S : U -> U.       (* symmetric *)
      Variable e : U.            (* neutral   *)
     
      Definition associative :=
        forall x y z: U, Op x (Op y z) = Op (Op x y) z.
     
      Definition commutative :=
        forall x y: U, Op x y = Op y x.
     
      Definition left_neutral :=
        forall x: U, Op e x = x.
     
      Definition right_neutral :=
        forall x: U, Op x e = x.
     
      Definition neutral :=
        left_neutral /\ right_neutral.
     
      Definition left_symmetric :=
        forall x: U, Op (S x) x = e.
     
      Definition right_symmetric :=
        forall x: U, Op x (S x) = e.
     
      Definition symmetric :=
        left_symmetric /\ right_symmetric.
     
      End operations. 
     
    End Operation.

    Ensuite un type de module pour les groupes ressemble à :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    Module Type Group.
     
      Import Operation.
     
      Parameter U : Set. 
      Parameter law : Operation U.  
      Parameter unit : U.
      Parameter inverse : U -> U.
     
      Axiom     law_associative : associative U law.
      Axiom     unit_neutral : neutral U law unit.
      Axiom     inverse_symmetric : symmetric U law inverse unit.
     
    End Group.
    Où là encore le paramètre U qu'on se trimballe partout peut lui aussi être rendu implicite.

    Un produit de deux groupes (j'ai effacé les preuves) :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    16
    17
    18
    19
    Module ProductGroup (G H : Group) : Group.
     
      Import Operation.
     
      Record GHU : Set := make {g : G.U; h : H.U}.
     
      Definition U := GHU. 
      Definition unit := make G.unit H.unit.
      Definition law x y := make (G.law x.(g) y.(g)) (H.law x.(h) y.(h)).
      Definition inverse x := make (G.inverse x.(g)) (H.inverse x.(h)).
     
      Definition law_associative : associative U law.
        Admitted.
      Definition unit_neutral : neutral U law unit.
        Admitted.
      Definition inverse_symmetric : symmetric U law inverse unit.
        Admitted.
     
    End ProductGroup.
    La limitation des modules est ailleurs: un module est une structure mais pas une valeur. C'est la raison pour laquelle les programmeurs Coq préfèrent les records et la coercion. Ils veulent que des structures puissent devenir des objets dans d'autres structures. Et ça n'est pas possible si la structure est un module.
    Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

+ Répondre à la discussion
Cette discussion est résolue.

Discussions similaires

  1. Pyreverse et liens entre classes
    Par PomFritz dans le forum Général Python
    Réponses: 0
    Dernier message: 03/02/2011, 22h44
  2. lien entre classes managed et unmanaged
    Par FadeOut dans le forum C++/CLI
    Réponses: 3
    Dernier message: 29/11/2010, 22h07
  3. WebService et ComplexType : lien entre classes
    Par macben dans le forum JWS
    Réponses: 1
    Dernier message: 01/10/2009, 11h11
  4. liens entre classes
    Par gate35 dans le forum Débuter
    Réponses: 7
    Dernier message: 28/05/2009, 18h01
  5. Réponses: 7
    Dernier message: 28/04/2009, 18h46

Partager

Partager
  • Envoyer la discussion sur Viadeo
  • Envoyer la discussion sur Twitter
  • Envoyer la discussion sur Google
  • Envoyer la discussion sur Facebook
  • Envoyer la discussion sur Digg
  • Envoyer la discussion sur Delicious
  • Envoyer la discussion sur MySpace
  • Envoyer la discussion sur Yahoo