Quelle est la réponse de programmation fonctionnelle aux invariants basés sur le type?

9

Je suis conscient que le concept d'invariants existe dans plusieurs paradigmes de programmation. Par exemple, les invariants de boucle sont pertinents en OO, en programmation fonctionnelle et procédurale.

Cependant, un type très utile trouvé dans la POO est un invariant des données d'un type particulier. C'est ce que j'appelle des "invariants basés sur le type" dans le titre. Par exemple, un Fractiontype peut avoir un numeratoret denominator, avec l'invariant que leur pgcd est toujours 1 (c'est-à-dire que la fraction est sous une forme réduite). Je ne peux garantir cela qu'en ayant une sorte d'encapsulation du type, sans laisser ses données être définies librement. En retour, je n'ai jamais à vérifier si elle est réduite, je peux donc simplifier les algorithmes comme les contrôles d'égalité.

D'un autre côté, si je déclare simplement un Fractiontype sans fournir cette garantie par encapsulation, je ne peux pas écrire en toute sécurité des fonctions sur ce type qui supposent que la fraction est réduite, car à l'avenir quelqu'un d'autre pourrait venir et ajouter un moyen de mettre la main sur une fraction non réduite.

Généralement, l'absence de ce type d'invariant peut conduire à:

  • Algorithmes plus complexes car les conditions préalables doivent être vérifiées / assurées à plusieurs endroits
  • Violations SÈCHES car ces conditions préalables répétées représentent la même connaissance sous-jacente (que l'invariant doit être vrai)
  • Devoir appliquer des conditions préalables par des échecs d'exécution plutôt que des garanties au moment de la compilation

Donc ma question est quelle est la réponse de programmation fonctionnelle à ce genre d'invariant. Existe-t-il une manière fonctionnelle et idiomatique de réaliser plus ou moins la même chose? Ou y a-t-il un aspect de la programmation fonctionnelle qui rend les avantages moins pertinents?

Ben Aaronson
la source
de nombreux langages fonctionnels peuvent le faire trivialement ... Scala, F #, et les autres langages qui fonctionnent bien avec la POO, mais aussi Haskell ... fondamentalement, n'importe quel langage qui vous permet de définir des types et leur comportement le supporte.
AK_
@AK_ Je suis conscient que F # peut le faire (bien que l'IIRC nécessite un saut de cerceau mineur) et a deviné que Scala pourrait être un autre langage inter-paradigme. Intéressant que Haskell puisse le faire - vous avez un lien? Ce que je recherche vraiment, c'est la réponse fonctionnelle-idiomatique , plutôt que des langages spécifiques qui offrent une fonctionnalité. Mais bien sûr, les choses peuvent devenir assez floues et subjectives une fois que vous commencez à parler de ce qui est idiomatique, c'est pourquoi je l'ai laissé hors de question.
Ben Aaronson
Pour les cas où la précondition ne peut pas être vérifiée au moment de la compilation, il est idiomatique de vérifier le constructeur. Considérez une PrimeNumberclasse. Il serait trop coûteux d'effectuer plusieurs vérifications redondantes de primalité pour chaque opération, mais ce n'est pas une sorte de test qui peut être effectué au moment de la compilation. (Beaucoup d'opérations que vous aimeriez effectuer sur des nombres premiers, par exemple la multiplication, ne forment pas une fermeture , c'est-à-dire que les résultats ne sont probablement pas garantis premiers. (Publication en tant que commentaires car je ne connais pas moi-même la programmation fonctionnelle.)
rwong
Une question apparemment sans rapport, mais ... Les assertions ou les tests unitaires sont-ils plus importants?
rwong
@rwong Oui, de beaux exemples là-bas. En fait, je ne sais pas à 100% à quel point ultime vous conduisez.
Ben Aaronson

Réponses:

2

Certains langages fonctionnels tels que OCaml ont des mécanismes intégrés pour implémenter des types de données abstraits, imposant ainsi certains invariants . Les langues qui ne disposent pas de tels mécanismes reposent sur le fait que l'utilisateur «ne regarde pas sous le tapis» pour appliquer les invariants.

Types de données abstraits dans OCaml

Dans OCaml, les modules sont utilisés pour structurer un programme. Un module a une implémentation et une signature , cette dernière étant une sorte de résumé des valeurs et des types définis dans le module, tandis que la première fournit les définitions réelles. Cela peut être vaguement comparé au diptyque .c/.hfamilier aux programmeurs C.

À titre d'exemple, nous pouvons implémenter le Fractionmodule comme ceci:

# module Fraction = struct
  type t = Fraction of int * int
  let rec gcd a b =
    match a mod b with
    | 0 -> b
    | r -> gcd b r

  let make a b =
   if b = 0 then
     invalid_arg "Fraction.make"
   else let d = gcd (abs a) (abs b) in
     Fraction(a/d, b/d)

  let to_string (Fraction(a,b)) =
    Printf.sprintf "Fraction(%d,%d)" a b

  let add (Fraction(a1,b1)) (Fraction(a2,b2)) =
    make (a1*b2 + a2*b1) (b1*b2)

  let mult (Fraction(a1,b1)) (Fraction(a2,b2)) =
    make (a1*a2) (b1*b2)
end;;

module Fraction :
  sig
    type t = Fraction of int * int
    val gcd : int -> int -> int
    val make : int -> int -> t
    val to_string : t -> string
    val add : t -> t -> t
    val mult : t -> t -> t
  end

Cette définition peut maintenant être utilisée comme ceci:

# Fraction.add (Fraction.make 8 6) (Fraction.make 14 21);;
- : Fraction.t = Fraction.Fraction (2, 1)

N'importe qui peut produire directement des valeurs de la fraction de type, en contournant le filet de sécurité intégré Fraction.make:

# Fraction.Fraction(0,0);;
- : Fraction.t = Fraction.Fraction (0, 0)

Pour éviter cela, il est possible de masquer la définition concrète du type Fraction.tcomme ça:

# module AbstractFraction : sig
  type t
  val make : int -> int -> t
  val to_string : t -> string
  val add : t -> t -> t
  val mult : t -> t -> t
end = Fraction;;

module AbstractFraction :
sig
  type t
  val make : int -> int -> t
  val to_string : t -> string
  val add : t -> t -> t
  val mult : t -> t -> t
end

La seule façon de créer un AbstractFraction.test d'utiliser la AbstractFraction.makefonction.

Types de données abstraits dans le schéma

Le langage Scheme n'a pas le même mécanisme de types de données abstraits qu'OCaml. Il repose sur l'utilisateur «ne regardant pas sous le tapis» pour réaliser l'encapsulation.

Dans Scheme, il est habituel de définir des prédicats comme la fraction?reconnaissance de valeurs donnant la possibilité de valider l'entrée. D'après mon expérience, l'usage dominant est de laisser l'utilisateur valider son entrée, s'il falsifie une valeur, plutôt que de valider l'entrée dans chaque appel de bibliothèque.

Il existe cependant plusieurs stratégies pour appliquer l'abstraction des valeurs renvoyées, comme renvoyer une fermeture qui donne la valeur lorsqu'elle est appliquée ou renvoyer une référence à une valeur dans un pool géré par la bibliothèque - mais je n'en ai jamais vu en pratique.

Michael Le Barbier Grünewald
la source
+1 Il convient également de mentionner que toutes les langues OO n'imposent pas l'encapsulation.
Michael Shaw
5

L'encapsulation n'est pas une fonctionnalité fournie avec la POO. Tout langage qui prend en charge une modularisation appropriée l'a.

Voici à peu près comment vous le faites à Haskell:

-- Rational.hs
module Rational (
    -- This is the export list. Functions not in this list aren't visible to importers.
    Rational, -- Exports the data type, but not its constructor.
    ratio,
    numerator,
    denominator
    ) where

data Rational = Rational Int Int

-- This is the function we provide for users to create rationals
ratio :: Int -> Int -> Rational
ratio num den = let (num', den') = reduce num den
                 in Rational num' den'

-- These are the member accessors
numerator :: Rational -> Int
numerator (Rational num _) = num

denominator :: Rational -> Int
denominator (Rational _ den) = den

reduce :: Int -> Int -> (Int, Int)
reduce a b = let g = gcd a b
             in (a `div` g, b `div` g)

Maintenant, pour créer un Rational, vous utilisez la fonction ratio, qui applique l'invariant. Parce que les données sont immuables, vous ne pouvez plus violer l'invariant par la suite.

Cela vous coûte cependant quelque chose: il n'est plus possible pour l'utilisateur d'utiliser la même déclaration de déconstruction que l'utilisation du dénominateur et du numérateur.

Sebastian Redl
la source
4

Vous procédez de la même manière: créez un constructeur qui applique la contrainte et acceptez d'utiliser ce constructeur chaque fois que vous créez une nouvelle valeur.

multiply lhs rhs = ReducedFraction (lhs.num * rhs.num) (lhs.denom * rhs.denom)

Mais Karl, dans OOP, vous n'êtes pas obligé d' accepter d'utiliser le constructeur. Oh vraiment?

class Fraction:
  ...
  Fraction multiply(Fraction lhs, Fraction rhs):
    Fraction result = lhs.clone()
    result.num *= rhs.num
    result.denom *= rhs.denom
    return result

En fait, les opportunités pour ce type d'abus sont moins nombreuses en PF. Vous devez mettre le constructeur en dernier, en raison de l'immuabilité. Je souhaite que les gens cessent de penser à l'encapsulation comme une sorte de protection contre des collègues incompétents, ou comme évitant la nécessité de communiquer des contraintes. Ça ne fait pas ça. Cela limite simplement les endroits que vous devez vérifier. Les bons programmeurs FP utilisent également l'encapsulation. Il se présente simplement sous la forme de la communication de quelques fonctions préférées pour effectuer certains types de modifications.

Karl Bielefeldt
la source
Eh bien, il est possible (et idiomatique) d'écrire du code en C #, par exemple, ce qui ne permet pas ce que vous avez fait là-bas. Et je pense qu'il y a une différence assez claire entre une seule classe responsable de l'application d'un invariant et chaque fonction écrite par n'importe qui, n'importe où qui utilise un certain type devant appliquer le même invariant.
Ben Aaronson
@BenAaronson Remarquez une différence entre "appliquer" et "propager" un invariant.
rwong
1
+1. Cette technique est encore plus puissante en FP car les valeurs immuables ne changent pas; ainsi vous pouvez prouver les choses "une fois pour toutes" à l'aide de types. Ce n'est pas possible avec des objets modifiables car ce qui est vrai pour eux maintenant peut ne pas l'être plus tard; du mieux que vous pouvez faire, revérifiez défensivement l'état de l'objet.
Doval
@Doval, je ne le vois pas. Mis à part le fait que la plupart des (?) Principaux langages OO ont un moyen de rendre les variables immuables. Dans OO, j'ai: Créer une instance, puis ma fonction mute les valeurs de cette instance d'une manière qui peut ou non être conforme à l'invariant. Dans FP, j'ai: Créer une instance, puis ma fonction crée une deuxième instance avec des valeurs différentes d'une manière qui peut ou non être conforme à l'invariant. Je ne vois pas comment l'immuabilité m'a aidé à me sentir plus confiant que mon invariant est conforme à toutes les instances du type
Ben Aaronson
2
@BenAaronson Immutability ne vous aidera pas à prouver que vous avez correctement implémenté votre type (c'est-à-dire que toutes les opérations préservent un invariant donné). Ce que je dis, c'est qu'il vous permet de propager des faits sur les valeurs. Vous encodez une condition (par exemple, ce nombre est pair) dans un type (en le vérifiant dans le constructeur) et la valeur produite est la preuve que la valeur d'origine satisfait la condition. Avec des objets mutables, vous vérifiez l'état actuel et conservez le résultat dans un booléen. Ce booléen n'est valable que tant que l'objet n'est pas muté de sorte que la condition est fausse.
Doval