Ouvrez http://127.0.0.1:8000/account/login/ dans votre navigateur. Vous devriez voir une page de connexion. Entrez un identifiant et un mot de passe valides. Vous verrez ce qui suit :

Vous pouvez voir que la section Mon tableau de bord est mise en évidence avec CSS car elle possède une classe choisi. Une fois l'utilisateur authentifié, le nom d'utilisateur est affiché sur le côté droit de l'en-tête. Cliquer sur le lien Se déconnecter. Vous verrez la page suivante :

Sur cette page, vous pouvez voir que l'utilisateur est déconnecté et que le menu du site Web n'est donc plus affiché. Le lien sur le côté droit de l'en-tête s'affiche désormais Se connecter.

Si vous voyez la page de déconnexion du site d'administration de Django plutôt que votre propre page de déconnexion, vérifiez vos paramètres INSTALLED_APPS et assurez-vous que django.contrib.admin c'est après compte. Les deux modèles se trouvent dans le même chemin relatif et le chargeur de modèles Django utilisera le premier qu'il trouvera.

Principalement pour développer des interfaces utilisateur. Pour l'utiliser, vous devez créer un type Modèle qui représente l'état complet du programme, un type Message qui décrit les événements environnementaux externes auxquels le programme doit répondre en changeant son état, une fonction de mise à jour qui crée un nouvel état du programme. à partir de l'ancien état et du message, et une fonction de visualisation qui, en fonction de l'état du programme, calcule les impacts requis sur l'environnement externe, qui génèrent des événements de type Message. Le modèle est très pratique, mais il présente un petit inconvénient : il ne vous permet pas de décrire quels événements ont du sens pour des états de programme spécifiques.

Un problème similaire se pose (et est résolu) lors de l’utilisation du modèle State OO.

Le langage Elm est simple, mais très strict : il vérifie que la fonction de mise à jour gère d'une manière ou d'une autre toutes les combinaisons possibles d'états de modèle et d'événements de message. Par conséquent, vous devez écrire du code supplémentaire, quoique trivial, qui laisse généralement le modèle inchangé. Je veux démontrer comment cela peut être évité dans des langages plus complexes - Idris, Scala, C++ et Haskell.

Tout le code présenté ici est disponible sur GitHub pour expérimentation. Regardons les endroits les plus intéressants.

MUV est un constructeur. Il accepte des paramètres : model - l'état initial du programme, updater - une fonction de mise à jour de l'état lors d'un événement externe et view - une fonction de création d'une vue externe. Notez que le type des fonctions de mise à jour et d'affichage dépend de la valeur du modèle (en utilisant la fonction msg à partir des paramètres de type).

Voyons maintenant comment lancer cette application

MuvRun : (Application modelType msgType IO) -> IO a muvRun (vue de mise à jour du modèle MUV) = do msg<- view model muvRun (MUV (updater model msg) updater view)
Nous avons choisi une opération d'entrée/sortie comme représentation externe (vue) (dans Idris, comme dans Haskell, les opérations d'entrée/sortie sont des valeurs de première classe ; pour qu'elles soient exécutées, des actions supplémentaires doivent être entreprises, renvoyant généralement une telle opération de la fonction principale).

En bref sur IO

Lors de l'exécution d'une opération de type (IO a), un certain impact sur le monde extérieur se produit, éventuellement vide, et une valeur de type a est renvoyée au programme, mais les fonctions de la bibliothèque standard sont conçues de telle manière qu'elle puisse être traité uniquement en générant une nouvelle valeur de type IO b. De cette façon, les fonctions pures sont séparées des fonctions ayant des effets secondaires. C'est inhabituel pour de nombreux programmeurs, mais cela permet d'écrire du code plus fiable.

Décrivons maintenant les types d'entités avec lesquelles nous allons travailler

Modèle de données = Déconnecté | Données de chaîne connectées MsgOuted = Données de chaîne de connexion MsgIned = Déconnexion | Accueil msgType total : Modèle -> Type msgType Logouted = MsgOuted msgType (Connecté _) = MsgIned
Nous décrivons ici un type de modèle qui reflète la présence de deux états d'interface : l'utilisateur n'est pas connecté et l'utilisateur avec un nom de type String est connecté.

Nous décrivons ensuite deux différents types de messages pertinents pour différentes variantes du modèle - si nous sommes déconnectés, nous ne pouvons nous connecter que sous un certain nom, et si nous sommes déjà connectés, nous pouvons soit nous déconnecter, soit dire bonjour. Idris est un langage fortement typé qui ne permet pas de mélanger différents types.

Et enfin, une fonction qui définit la correspondance de la valeur du modèle avec le type de message.

La fonction est déclarée totale - c'est-à-dire qu'elle ne doit pas planter ou se bloquer, le compilateur essaiera de surveiller cela. msgType est appelé au moment de la compilation, et sa totalité signifie que la compilation ne se bloquera pas à cause de notre erreur, bien qu'elle ne puisse pas garantir que l'exécution de cette fonction épuisera les ressources du système.
Il est également garanti qu'il n'exécutera pas "rm -rf /" car il n'y a pas d'IO dans sa signature.

Décrivons le programme de mise à jour :

Programme de mise à jour total : (m:Modèle) -> (msgType m) -> Programme de mise à jour du modèle Déconnecté (Nom de connexion) = Nom de connexion du programme de mise à jour (Nom de connexion) Déconnexion = Programme de mise à jour déconnecté (Nom de connexion) Greet = Nom de connexion
Je pense que la logique de cette fonction est claire. Je voudrais souligner encore une fois la totalité - cela signifie que le compilateur Idris vérifiera que nous avons pris en compte toutes les alternatives autorisées par le système de types. Elm effectue également cette vérification, mais il ne peut pas savoir que nous ne pouvons pas nous déconnecter si nous ne sommes pas encore connectés et nécessitera un traitement explicite de la condition.

Programme de mise à jour déconnecté Déconnexion = ???
Idris trouvera des incompatibilités de type lors d'une vérification inutile.

Passons maintenant à la vue - comme d'habitude dans l'interface utilisateur, ce sera la partie la plus difficile du code.

Total loginPage : IO MsgOuted loginPage = do putStr "Login : " map Login getLine total genMsg : String -> MsgIned genMsg "" = Déconnexion genMsg _ = Saluer total workPage : String -> IO MsgIned workPage name = do putStr ("Bonjour, " ++ nom ++ "\n") putStr "Saisissez une chaîne vide pour la déconnexion ou non vide pour le message d'accueil\n" map genMsg getLine vue totale : (m : modèle) -> vue IO (msgType m) Logouted = loginPage view (Nom de connexion ) = nom de la page de travail
view doit créer une opération d’E/S qui renvoie des messages, dont le type dépend encore une fois de la valeur du modèle. Nous avons deux options : loginPage, qui imprime un message "Login :", lit une chaîne du clavier et l'enveloppe dans un message de connexion, et workPage avec un paramètre de nom d'utilisateur, qui imprime un message d'accueil et renvoie des messages différents (mais du même type). - MsgIned) selon que l'utilisateur saisit une chaîne vide ou non vide. view renvoie l'une de ces opérations en fonction de la valeur du modèle, et le compilateur vérifie leur type, même s'il est différent.

Nous pouvons maintenant créer et exécuter notre application

Application : Modèle d'application Main.msgType IO app = MUV Vue du programme de mise à jour déconnecté principale : IO () main = application muvRun
Un point subtil doit être noté ici : la fonction muvRun renvoie IO un, où a n'a pas été spécifié et la valeur main est de type IO(), Où () est le nom d'un type habituellement appelé Unité, qui a une valeur unique, également écrite sous forme de tuple vide () . Mais le compilateur peut gérer cela facilement. en remplaçant a() à la place.

Types Scala et dépendants du chemin

Classe abstraite scellée Classe de cas MsgLogouted Login (nom : chaîne) étend la classe abstraite scellée MsgLogouted Classe de cas MsgLogined Logout() étend la classe de cas MsgLogined Greet() étend la classe abstraite MsgLogined View ( def run() : Msg ) classe abstraite scellée Modèle ( type Message def view() : View ) la classe de cas Logouted() étend le modèle (type Message = MsgLogined remplace la vue def() : View .... ) la classe de cas Logined(nom : String) étend le modèle (type Message = MsgLogined remplace la vue def( ): Voir .... )
Les types algébriques dans Scala sont modélisés par héritage. Le type correspond à certains classe abstraite scellée, et chaque constructeur en a hérité classe de cas. Nous allons essayer de les utiliser exactement comme des types algébriques, décrivant toutes les variables comme appartenant au parent classe abstraite scellée.

Les classes MsgLogined et MsgLogouted de notre programme n'ont pas d'ancêtre commun. La fonction de visualisation devait être répartie sur différentes classes du modèle afin d'avoir accès à un type de message spécifique. Cela a ses avantages, que les partisans d'OO apprécieront : le code est regroupé selon la logique métier, tout ce qui concerne un cas d'utilisation est à proximité. Mais je préfère séparer le regard en une fonction distincte, dont le développement pourrait être transféré à une autre personne.

Maintenant, implémentons le programme de mise à jour

Objet Updater ( def update(model: Model)(msg: model.Message) : Model = ( correspondance du modèle ( case Logouted() => msg match ( case Login(name) => Logined(name) ) case Logined(name) => correspondance du msg ( case Logout() => Logouted() case Greet() => model ) ) ) )
Ici, nous utilisons des types dépendants du chemin pour décrire le type du deuxième argument à partir de la valeur du premier. Pour que Scala accepte de telles dépendances, les fonctions doivent être décrites sous forme curry, c'est-à-dire comme une fonction du premier argument, qui renvoie une fonction du deuxième argument. Malheureusement, Scala n'effectue pas actuellement beaucoup de vérifications de type pour lesquelles le compilateur dispose de suffisamment d'informations.

Donnons maintenant une implémentation complète du modèle et de la vue

La classe de cas Logouted() étend le modèle ( tapez Message = MsgLogouted override def view() : View = new View ( override def run() = ( println("Enter name ") val name = scala.io.StdIn.readLine() Connexion (nom) ) ) case class Logined(name: String) extends Model ( type Message = MsgLogined override def view() : View = new View ( override def run() = ( println(s"Bonjour, $name") println ( "Chaîne vide pour la déconnexion, non empy pour le message d'accueil.") scala.io.StdIn.readLine() match ( case "" => Logout() case _ => Greet() ) ) ) classe abstraite View ( def run( ) : Msg ) Visionneuse d'objets ( def view(model: Model): View = ( model.view() ) )
Le type de retour d'une fonction de vue dépend de l'instance de son argument. Mais pour la mise en œuvre, on se tourne vers le modèle.

L'application ainsi créée se lance ainsi :

Objet principal ( import scala.annotation.tailrec @tailrec def process(m: Model) ( val msg = Viewer.view(m).run() process(Updater.update(m)(msg)) ) def main(args: Tableau) = (processus (Déconnecté()) ) )
Le code système d'exécution ne sait donc rien de la structure interne des modèles et des types de messages, mais le compilateur peut vérifier que le message correspond au modèle actuel.

Ici, nous n'avions pas besoin de toutes les capacités fournies par les types dépendants du chemin. Des propriétés intéressantes apparaîtront si l’on travaille en parallèle avec plusieurs instances de systèmes Model-Updater-View, par exemple lors de la simulation d’un monde multi-agents (la vue représenterait alors l’influence de l’agent sur le monde et la réception de feedback). Dans ce cas, le compilateur a vérifié que le message a été traité exactement par l'agent auquel il était destiné, malgré le fait que tous les agents ont le même type.

C++

Les types algébriques peuvent être implémentés de la même manière qu'en Scala - une classe abstraite correspond à un type, et les descendants concrets correspondent aux constructeurs (appelons-les « classes de constructeurs », pour ne pas être confondus avec les constructeurs C++ ordinaires) du type algébrique. taper.

C++ prend en charge les types dépendants du chemin, mais le compilateur ne peut pas utiliser le type dans l'abstrait sans connaître le type réel auquel il est associé. Par conséquent, il est impossible d'implémenter Model-Updater-View avec leur aide.

Mais C++ dispose d’un puissant système de modèles. La dépendance du type à la valeur du modèle peut être masquée dans un paramètre de modèle d'une version spécialisée du système exécutif.

Processeur Struct ( Processeur const virtuel *next() const = 0; ); modèle struct ProcessorImpl : processeur public ( const CurModel * modèle ; ProcessorImpl (const CurModel* m) : modèle(m) ( ); const Processeur *next() const ( const Vue * view = modèle->view(); const typename CurModel::Message * msg = view->run(); supprimer la vue ; const Modèle * newModel = msg->process(model); supprimer le message ; return newModel->processor(); ) );
Nous décrivons un système d'exécution abstrait, avec une méthode unique pour faire tout ce qui est requis et renvoyer un nouveau système d'exécution adapté à l'itération suivante. La version spécifique possède un paramètre de modèle et sera spécialisée pour chaque « classe de constructeur » du modèle. Il est important ici que toutes les propriétés de type CurModel soient vérifiées lors de la spécialisation du modèle avec un paramètre de type spécifique, et au moment de la compilation du modèle lui-même, il n'est pas nécessaire de les décrire (bien qu'il soit possible d'utiliser concepts ou d'autres moyens d'implémenter des classes de types). Scala dispose également d'un système assez puissant de types paramétrés, mais il vérifie les propriétés des types de paramètres lors de la compilation du type paramétré. Là, la mise en œuvre d'un tel modèle est difficile, mais possible, grâce au support des classes de types.

Décrivons le modèle.

Modèle Struct ( virtual ~Model() (); virtual const Processeur *processor() const = 0; ); struct Connecté : modèle public ( struct Message ( const modèle virtuel * process(const Connecté * m) const = 0; virtual ~Message() (); struct Déconnexion : message public ( const Model * process(const Connecté * m) const; struct Greet: public Message ( const Model * process(const Logined * m) const; ); const std::string name; (...); vue const * view() const ( return new LoginedView(name); ); const Processeur *processor() const (retourne un nouveau ProcessorImpl (ce); (...); vue const ); ); struct Déconnecté : modèle public ( struct Message ( const modèle virtuel * processus (const déconnecté * m) const = 0; virtuel ~Message() (); struct Connexion : message public ( const std::nom de chaîne; Connexion (std :: string lname) : name(lname) ( ); const Modèle * process(const Déconnecté * m) const ; * view() const ( return new LogoutedView(); ); const Processeur *processor() const (retourne un nouveau ProcessorImpl
(ce);

); );

Modèle Const * Logouted::Login::process(const Logouted * m) const ( delete m; return new Logined(name); ); const Modèle * Logined::Logout::process(const Logined * m) const ( delete m; return new Logouted(); ); const Modèle * Logined::Greet::process(const Logined * m) const ( return m; );
Rassemblons maintenant tout ce qui concerne la vue, y compris les entités internes des modèles

Modèle struct View ( message const virtuel * run() const = 0; virtuel ~View () (); ); struct Connecté : modèle public ( struct LoginedView : vue publique ( const std::string name; LoginedView(std::string lname) : name(lname) (); virtual const Message * run() const ( char buf; printf("Bonjour %s", name.c_str()) ; fgets(buf, 15, stdin); return (*buf == 0 || *buf == "\n" || *buf == "\r") ? (nouvelle déconnexion()) : static_cast (nouveau salut); ); ); vue const * view() const ( return new LoginedView(name); ); ); struct Logouted : modèle public ( struct LogoutedView : vue publique ( virtual const Message * run() const ( char buf; printf("Connexion: "); fgets(buf, 15, stdin); return new Login(buf); ); ); vue const * view() const ( return new LogoutedView(); ); );
Et enfin, écrivons main

Int main(int argc, char ** argv) ( const Processeur * p = new ProcessorImpl (nouveau Déconnecté()); while(true) ( ​​​​const Processeur * pnew = p->next(); delete p; p = pnew; ) return 0; )

Et encore Scala, cette fois avec des classes de types

Partie similaire du code

classe abstraite View ( def run(): Message ) classe abstraite Processeur ( def next() : Processeur; ) classe abstraite scellée Modèle ( def processeur() : Processeur ) classe abstraite scellée Classe de cas LoginedMessage Logout() étend la classe de cas LoginedMessage Greet( ) étend la classe de cas LoginedMessage Logined (nom de valeur : String) étend le modèle (remplace le processeur def (): Processor = new ProcessorImpl (this)) classe abstraite scellée Classe de cas LogoutedMessage Login (nom : chaîne) étend la classe de cas LogoutedMessage Logouted () étend le modèle ( override def processeur() : Processeur = new ProcessorImpl(this) ) object Main ( import scala.annotation.tailrec @tailrec def process(p: Processor) ( process(p.next()) ) def main(args: Array) = (processus(nouveau ProcessorImpl(Déconnecté())) ) )

Classe ProcessorImpl(model: M)(mise à jour implicite: (M, Message) => Modèle, vue: M => View) extends Processor ( def next(): Processor = ( val v = view(model) val msg = v. run() val newModel = updater(model,msg) newModel.processor() ) )
Ici nous voyons de nouveaux paramètres mystérieux (mise à jour implicite : (M, Message) => Modèle, vue : M => Vue). Le mot-clé implicite signifie que lors de l'appel de cette fonction (plus précisément, le constructeur de classe), le compilateur recherchera des objets de types appropriés marqués comme implicites dans le contexte et les transmettra comme paramètres appropriés. Il s'agit d'un concept assez complexe dont l'une des applications est l'implémentation de classes de types. Ici, ils promettent au compilateur que pour des implémentations spécifiques du modèle et du message, nous fournirons toutes les fonctions nécessaires. Maintenant, tenons cette promesse.

Mises à jour d'objets ( implicite def logoutedUpdater(model: Logouted, msg: LogoutedMessage): Model = ( (model, msg) match ( case (Logouted(), Login(name)) => Logined(name) ) ) implicite def viewLogouted(model : Logouted) = new View (remplacer def run() : LogoutedMessage = ( println("Enter name ") val name = scala.io.StdIn.readLine() Login(name) ) ) implicite def loginedUpdater(model: Connecté, msg : LoginedMessage): Model = ( (model, msg) match ( case (Logined(name), Logout()) => Logouted() case (Logined(name), Greet()) => model ) ) implicite def viewLogined( model: Connecté) = new View ( val name = model.name override def run() : LoginedMessage = ( println(s"Bonjour, $name") println("Chaîne vide pour la déconnexion, nonempy pour le message d'accueil.") scala.io .StdIn.readLine() match ( case "" => Logout() case _ => Greet() ) ) ) importer les mises à jour._

Haskell

Modèle de données = pour tous m. (M pouvant être mis à jour, m visualisable) => Classe modèle m M pouvant être mis à jour où données Message m:: * update:: m -> (Message m) -> Classe de modèle (M pouvant être mis à jour) => M visualisable où vue :: m -> (Afficher (Message m)) données Déconnecté = Données déconnectées Connecté = Chaîne connectée
J'ai essayé de séparer le programme de mise à jour et l'affichage autant que possible, j'ai donc créé deux classes de types différentes, mais jusqu'à présent, cela n'a pas bien fonctionné.

L'implémentation du programme de mise à jour est simple

Instance pouvant être mise à jour Déconnectée où les données Message Déconnecté = Mise à jour de la chaîne de connexion Déconnecté (Nom de connexion) = Modèle (Nom de connexion) Instance pouvant être mise à jour Connecté où les données Message Connecté = Déconnexion | Mise à jour du message d'accueil m Déconnexion = Modèle Mise à jour déconnectée m Message d'accueil = Modèle m
J'ai dû corriger IO en tant que View. Les tentatives pour le rendre plus abstrait ont tout compliqué et augmenté le couplage du code - le type Model doit savoir quelle vue nous allons utiliser.

Importer le type System.IO View a = IO une instance Visualisable Déconnecté où view Logouted = do putStr "Connexion : " hFlush stdout fmap Connexion getLine instance Visualisable Connecté où view (Nom connecté) = do putStr $ "Bonjour " ++ nom ++ " !\n" hFlush sortie standard l<- getLine pure $ if l == "" then Logout else Greeting
Eh bien, l'environnement exécutable diffère peu de celui similaire d'Idris

RunMUV :: Model -> IO a runMUV (Modèle m) = faire msg<- view m runMUV $ update m msg main:: IO () main = runMUV (Model Logouted)