Deriving equations always have been a fascinating thing, due to current project requirement I recently started reading All of Statistics, in several chapters it omit some proofs which I'm going to outline here

The properties of conditional expectations.

First we lay down the definition of conditional expectations, if and are two random variables, then

where , as expected.

Notice that is itself a function of , and itself can be functions, just like in normal expectations, we have

This is in fact a not so obvious result, because normally by definition of expectation we should have

The proof I will omitted here but it's nonetheless named Law of unconscious statistician. Today we simply want to discuss some of its properties, which are easy and fun to derive while remaining not-so-trivial.

Theorem 1: , where is a constant.

Proof: 

(1)  

The author mentioned specifically about the regression problem, we use the function to represent the result of the regression, and if is the random variable of the value on the de facto curve, then we can use the random variable to represent the error between the result of regression and the real curve, the books says that if we let , then . To show this, we need first to establish a lemma.

Lemma 1:

Proof:  

(2)  

Notice in the first step, since is a function of , thus when we expand the outer expectation we are actually expanding for some , thus we first integrating w.r.t. , and when we expand further the inner expectation itself, by definition it's an expectation of so we are integrating w.r.t. . Now, since itself is a constant w.r.t. , we can move it inside the inner integral, and furthermore, in statistics we often make some aggressive assumptions, for example, here we suppose that the iterated integral automatically satisfies the Fubini's theorem, thus we can exchange their order,

(3)  

But notice that is just ,and since is constant w.r.t. we can move it out of the inner integral, thus

(4)  

Having proven this, we need to prove another lemma, that is the linearity of conditional expectation, which the author also lacks in the original text

Lemma 2:

Proof:

(5)  

Now we can prove that by noticing that

(6)  

This means that the error between the result of regression and the actual curve can be modeled by a distribution whose expectation is , in fact, you should have no surprise that normally the error is modeled by a normal distribution centered at , i.e. . That is, every curve regression problem can be modeled by the result of regression, plus a perturbation function that follows the normal distribution centered at .

Cet article court vise à expliquer d'une manière formelle ces concepts, avec une bonne intuition afin qu'on ne se perde pas dans le formalisme. 

On n'a pas besoin du mesure aujourd'hui, cela va finir bientôt. On parle désormais à l'intérieur d'un univers , et on peut prendre des échantillons depuis . On arrive souvent à notre premier malentendu ici: un échantillon, ce n'est pas un individuel dans l'univers, en revanche, le résultat d'un échantillonnage parcourrait l'univers plénier, alors on traite un échantillon comme une fonction au profit de le bien décrire, cette fonction, c'est un variable aléatoire , il est une fonction de dans (et certes, en principe on se permet de choisir d'autres espaces tant qu'il est mesurable). Cet étape nous laisse de voir des échantillons et des évènement arbitraires comme l'apparence des nombres; dit simplement, les variables aléatoires bâtissent un pont entre le monde non-mathématique à celui qui est. Avec les variables aléatoires on peut écrire des probabilité des évènements arbitraires comme celles des évènements de nombres , un évènement, c'est un ensemble où est un prédicat.

Maintenant on se tourne vers la fonction de densité et la fonction de loi, prenons comme un exemple un dé fair, les chances de tirer chaque nombre entre et sont équiprobables, alors l'univers c'est , soit   un variable sur cet univers, et soit 

si tu as une fois appris la probabilité, tu reconnais immédiatement que " suit un loi binomiale", mais qu'est-ce que cela veut dire? Remarques que envoie à et à , si on dessine cette application dans un diagramme, tu verras une ligne grêle à avec une hauteur , et c'est la fonction de densité, elle veut essentiellement dire que "combien d'échantillons le variable a-t-il envoyé à ce résultat, par rapport à l'univers plénier?".

On peut également se tourner vers le cas continu, e.g., soit suit une loi normale, dit, les hauteurs humaines, et supposons qu'on contrôle l'hauteur humaine par deux gènes indépendants: et , et chacun des gènes peut prendre beaucoup de valeurs: et , alors l'univers sera

et sera une telle fonction qui envoie une combinaison de gènes à un nombre (l'hauteur). Par exemple, il enverrait à l'hauteur "180cm". La fonction n'est pas fidèle: elle est tout à fait possible d'envoyer deux combinaisons à la même hauteur; puisque l'hauteur est une valeur continue, on dit toujours un intervalle d'hauteurs, au lieu d'une valeur précise, et du coup, envoie, par exemple, à , et envoie à , envoie à , etc.., et finalement, la phrase " suit une loi normale" dit que si on compte les tailles de , on trouvera que est plus grand, ensuite et , et puis d'autre intervalles. si on les range en une ligne par intervalles, ils forment une courbe en cloche, cette courbe est la fonction de densité de la loi normale, et également, elle veut dire que "combien d'échantillons le variable a-t-il envoyé dans cet intervalle, par rapport à l'univers plénier."

Et finalement c'est le moment pour expliquer la notation , , en soi-même, c'est une fonction qui accepte un évènement et, souviens-toi qu'un évènement, c'est simplement une partir , par conséquent serait aussi une partie de , on arrive à le faire d'une façons la plus directe, soit 

et plus généralement, soit un prédicat arbitraire sur , on écrit pour

Et enfin on est assez prêt pour expliquer la convergence en probabilité, on dit que une séquence de variables converge vers un variable en probabilité si 

Au profit de la simplicité, ignorons la fonction absolue, qu'est-ce que veut dire? Si on insiste à utiliser l'exemple de l'hauteur, on sait que et nous disent approximativement "j'enverrai une combinaison de gènes à quelle hauteur?", et par conséquent nous montre la distance entre les hauteurs auxquelles elles ont envoyées. Depuis ce point de vue, nous dit que la probabilité que cette distance dépasse finira par . Et si on se tourne vers un point de vue plus formel, on demande: quelle est la fonction de densité du variable ? Remarques que signifie que "la distance des hauteurs affectées par ces deux variables est plus grande que ", du coup par notre interprétation auparavant, la fonction de densité de nous montre "combien de combinaison de gènes dont la distance des hauteurs affectées par et tombe dans chaque intervalle, par rapport à l'univers plénier?", et par suite exige clairement que le nombre approximatif de combinaison de gènes dont la distance des hauteurs affectées par et dépasse devrait finir par .

Sur ce problème, bien sûr tu peux les organiser et les marquer des étiquettes en automonie, mais je n'ai pas beaucoup de temps libres quoi que ce soit, alors finalement j'ai fini par une décision un peu irrationnelle: Je arrêterai mes études d'un sujet mathématique et je me metterai à apprendre l'apprentissage automatique. Pour que je puisse les marquer et organiser automatiquement.

À la première vue tu dirais probablement "quel détour!", oui, si le but c'est simplement de développer un tel logiciel, cela ne rend pas nécessaire un étude profond et, en fait, tout le monde pourrrait le finir en un mois, mais je te répondrai "mais non", en faisant ça, cela m'apportera plusieurs avantages:

1. Le domaine auquel je veux appliquer, c'est néanmoins un programme informatique, et le sujet mathématique que je viens de renoncer, ce qui est les équations differentielles partielles. Mes connaissances des EDPs ne m'offrira aucun avantage quand mon CV est presenté au professeur, mais les expériences sur l'apprentissage automatique ainsi qu'un projet décent heurtera définiteivement le jackpot.
2. Cela n'intéressera personne, mais je suis, véritablement et authentiquement, un étudiant de mathématique, j'ai appris l'analyse de manifold, l'algèbre linéaire et abstraire, la topologie, etc... d'une façons beaucoup plus systématique que les étudiants d'ingénierie. On dit souvent que l'apprentissage automatique c'est un domaine de magique, mais il me restera peu de mystérie, car j'ai, depuis longtemps, l'habitude de comprendre la démonstration avant d'utiliser le résultat. Je dirais qu'il n'y ait guère étudiant non mathématique qui comprendre la méchanisme véritable du théorème de Stokes :)
3. L'initiation aux mathématique me permet d'avoir une vue spéctaculaire pour ce domaine, j'ai entendu depuis longtemps les recherches sur, par exemple, "l'apprentissage automatique géométrique" et j'ai vu une fois un article tentant d'interpreter la modèle en terme de la théorie des catégories, ces idées sont déjà intéressante simplement à y entendre. Imagines quel plaisir je prendrais à y apprendre.

Et ces raisons ferment notre discussion sur mon choix, il faut continuer nos études. Je viens de me trouver récemment que je ne suis pas en accord avec la probabilité, bien que je sois habitué à apprendre l'analyse, l'algèbre, etc..., je pense que c'est du fait que, une leçon d'introduction de probabilité commence souvent par un début pas trop axiomatique.

Aujourd'hui les systèmes de type fait l'objet de notre discussion, comme d'habitude.
  Je crois que toi, le lecteur ou la lectrice, n'a aucune nécessité pour être introduit du système HM, aujourd'hui on fait l'objet de notre discussion les Pros et Cons du système HM, et par ailleurs les problèmes on va rencontrer si l'on choisit d'autres systèmes que HM.

Quelle est la caractèristique du système HM?

On dit souvent du système HM, mais qu'est-ce que le système HM? dit simplement, HM est le système utilisé par le langage ML, et généralement on peut appeller aussi le système de OCaml comme le système HM. Caractérisé par l'utilisation, le HM est un système qui n'a pas besoin de tout annotation, et caractérisé par l'implémentation, le HM est un système qui utilise les types principaux, un résolveur global, avec la généralisation automatique sur les let-expressions.
  Bien, donc HM est bon, il est impeccable, donc pourquoi n'utilise-on pas le système HM partout? Parce que pour soutenir les avantages de HM, il faut circonscrire l'expressibilité du système, par exemple, on ne soutient pas le rank-n-polymorphism et le Higher Kinded Polymorphism

Ce sont quoi? le rank-n-polymorphism nous permet de généraliser la fonction d'ordre supérieur, par exemple, on peut écrire

f:\forall \sigma. (\forall \tau. \tau \to \sigma) \to \tt unit

remarquer comment le quantificateur $\tau$ apparaît à la position d'un paramètre, dans un système soutenant le rank-n-polymorphism, les quantificateurs sont permis d'apparaître arbitrairement profond, cependant, c'est célèbre que le rank-n-polymorphism où $n\ge 3$ est indécidable. C'est-à-dire rank-2-polymorphisme est encore un choix éligible pour la plupart du langage, cependant, HM ne soutient que le rank-1-polymorpshime, c'est-à-dire le polymorphisme parametrique le plus ordinaire, les quantificateurs ne sont permis d'apparaître qu'à la fonction le plus externe (on dit que c'est la forme prenex).
Quant au Higher Kinded Polymorphism, il permet les paramètres typages d'être des types généralisés.

Mais, ce sont très utile dans certaines circonstances, si nous les voulons, il ne faut pas utiliser l'algorithme HM.

Par ailleurs, le système HM adopt un algorithme global, ça nous dit que le système collecte les symboles dans la fonction entière pour construire un ensemble d'équations, et puis il résoud chaque variable typage dans cet ensemble. Ça fait un problème que, l'endroit où on résoud les équation est différent de l'endroit où on collecte les symboles, quand la résolution fait une erreur, elle ne peut pas rapporter la position précise dans le source, on dit que le système HM a un mauvais localité.

Pour résoudre ces problèmes, on a un autre algorithme, l'inférence locale, mais avant d'approfondir sur ce sujet, il faut expliquer qu'est-ce que le mot "locale" signifie ici.

L'inférence locale vs l'inférence globale

Durant l'inférence d'une fonction, il aura des locations où l'information typage est perdu, auquel il faut les inférer, pour l'inférence globale comme HM, une fonction comme ça peut être typé

function func1(a) {
    var s = a;
    return func2(s);
}

function func2(b) {
    return b += 10;
}

d'abord on assigne les types principaux aux variables, supposons que s: S', a: A', et b: B', depuis func2(b) on a B' = int et S' = B', depuis var s = a on a A' = S', en résoulvant cet ensemble d'équation nous donne b: int, s: int et a: int, easy peasy! Mais remarquer qu'on a collecté les équations globalement, i.e., l'information typage coule entre les noeuds fraternels, mais dans une inférence locale, l'information typage ne peut couler qu'entre les noeuds parentals, donc l'exemple ci-dessus ne peut pas typecheck par rapport à une inférence locale, parce que l'information obtenue depuis l'expression func2(b) ne peut pas couler à l'expression var s = a, donc c'est impossible de savoir le type de s en collectant l'information de func2(s).

C'est précisément pourquoi cette forme d'inférence s'appelle l'inférence locale, les Pros, c'est d'être plus simple que l'inférence globale, durant l'implémentation d'un tel algorithme, on peut trouver qu'on n'a pas en effet besoin de collecter les équations, tous les variables et tous les types perdus sont résoulus in situ, pour que l'exemple ci-dessue devienne éligible pour l'inférence locale, il faut annotater le paramètre a et b comme

function func1(a: int) {
    var s = a;
    return func2(s);
}

function func2(b: int) {
    return b += 10;
}

maintenant l'information typage ne coule que depuis les noeuds parentals aux noeuds fraternels, par exemple l'information a: int coule à l'expression var s = a, mais l'information de func(s) ne coule jamais à ni a ni var s = a.

et c'est pourquoi dans un langage comme C# ou Java, tu vois toujours des fonctions annotatées: de tels langages ne permettent pas de la fonction non annotée, ils ne peut pas les typecheck.
si tu as vu l'article par Pierce & Turner, tu vas savoir aussi que dans un tel algorithme on ne résoud les types qu'aux appels de fonction. Ça rend plus simple le processus de l'inférence, en échange d'un coût mineure: il faut annotater les paramètres.

De plus, l'inférence locale nous fournit une belle localité, puisque tous les variables sont résolu in situ, donc on peut rapporter des erruers dès qu'on les rencontre, ça rend plus bienveillant les messages d'erreur.

La bidirectionalité

  À part de la localité, l'inférence locale possède une autre caractéristique, c'est la bidirectionalité, puisque dans l'inférence locale on ne collecte jamais les équations, on les résoud in situ, donc il faut avoir un point auquel on peut créer une équation et la résoudre immediamment, au-dessus j'ai dit que c'est les appels de fonction, et c'est vrai, mais les chercheurs lui a donné un nom plus exotique: l'inférence locale bidirectionnel, c'est parce que si on voit les appels en vue de l'AST, on trouvera que un point auquel il est exactement un appel est répresenté par un noeud dans l'AST, dit FuncCall, et ses arguments sont les noeuds enfants, pour créer une équation à ce point, d'abord on trouve le type des arguments, puis on trouve le type de la fonction, par exemple, dans le code suivant:

function func<A, B, C>(a: A, b: B, c: C) { 
    // ...
}

func(1, "2", '3')

Le type de la fonction est $\forall\tt A, B, C. A \to B \to C \to \tt unit$ ou (en la forme uncurrié) $\tt \forall A, B, C. (A, B, C) \to \tt unit$, les type des arguments sont int, string, char respectivement, donc on crée trois équations

et on les résoud in situ pour obtenir l'instantiation de ces trois variables typages, depuis l'AST, ces arguments sont les noeuds enfants et l'appel de fonction func(...) est le noeud parental, donc on peut considerer comme si l'on fait concorder l'information typage au-dessous de ce point (i.e. les types des arguments) avec l'information typage au-dessus de ce point (i.e. le type de la fonction, c'est obtenu du environnement, donc on peut considerer qu'il vient d'un endroit plus haut dans l'AST), c'est deux direction des coulées d'information typage, donc on dit que c'est une inférence bidirectionnel.

Quel est le problème quand on étend l'inférence locale aux sous-types?

  HM, c'est pas très difficile à comprendre, l'inférence locale, c'est aussi. Mais notre discussion a été circonscrit dans un fragment système F pur, sans fait aucune référence à l'extension, maintenant on discute sur une extension particulièrement important et intéressant: le sous-typage.

La première modification le sous-typage fait à l'inférence, c'est de transformer les équations en les inégalités, maintenant au lieu de résoudre une équation comme A = int, il faut résoudre une inégalité comme nothing <: A <: any, A peut être tout type qui satisfait cette inégalité, et on vise à minimiser A, i.e., on trouve un type A tel qu'il soit le type minimal satisfaisant tous les inégalités le contenant, en combinant avec le système F, on dit que c'est le système F sub, écrit $F_{<:}$, ou on dit que c'est la quantification bornée.

Alors c'est tout? Non, le sous-typage fait le deuxième changement de notre système: dans une inférence locale d'un système F sub, pas seulement les coulées d'information typage entre les noeuds fraternels sont interdits, mais également les coulées qui contiennent d'information typage partielle, par exemple

où $g:\tt \forall X. (\mathtt{int} \to X) \to X$. Parce que information typage est incomplèt quand on typecheck x => x + 1.

Mais pourquoi ne peut-on pas faire ça? Ça nous semble parfaitement légal. La raison fondamentale de ça c'est que si l'on permet de telles coulées d'information, il nous entraînera peut-être aux résultats illégals, Voici la fonction

ou dans un lanage comme scala, on peut même écrire

def map[X, Y](f: X -> Y, list: List[X]): List[Y]

on peut l'appeler comme

val result: List[int] = map(x => x + 1, list)

où list: List[int]. Maintenant, si l'on traite les arguments en isolation, et on regarde seulement à x => x + 1, comment peut-on calculer le type de x? si on prend une façon plus conservative, la résponse ne peut pas devenir plus simple: non, on ne peut pas déduire ce qu'on peut typer x, parce qu'il n'y a pas d'information, si l'on devient plus aggresif, on peut même permettre de résoudre x depuis x + 1 et conclure que x doit être de type int.

Cette façon nous attire, mais ce n'est plus locale: on fait couler le type de x en arrière, de x + 1 à x, où le premier est plus haut dans l'AST et le dernier est plus bas, le coulant d'information typage traverse plus qu'un niveau. Donc pourquoi est-ce qu'on ne peut pas être plus agile et abandonner ce dogme, mélanger l'inference locale et globale? C'est parce que ça rend plus complexe et impuissante l'inférence locale: elle est désignée d'être un système qui est bien plus simple que l'inférence globale comme HM, deuxièmement, même si l'on permet de la rétropropagation (oui ici je ne fais aucune réference au même concept de ML), elle tend encore à avoir des problèmes, la raison c'est d'avoir le sous-types, par exemple, quand on résoud des inégalités de type, on tend à choisir le résolution le plus petite, ou on choisit un type arbitraire, si on a map(x => x + 1, list), et le typecheck est procédé en isolation (ce qui nous dit que le typecheck de x => x + 1 ne considère pas l'argument list), on peut déduire que ⊥ <: X <: int (parce que + accepte deux int et x est l'argument de +) et notre strategie nous donne la borne inférieur X = ⊥ et donc x: ⊥ et enfin ... on a list: List[⊥], ça n'est pas ce qu'on veut!

Donc, peut-on simplement maximiser au lieu de minimiser un variable typage obtenu de la rétropropagation? Oui peut-être, mais le problème fondamental est la complexité de cette conception viole le but initial de l'inférence locale: un système plus simple à implémenenter.

Cas 1e

Ou, on peut même abandonner la rétropropagation, et en revanche retarder le typecheck de x => x + 1, on typecheck l'argument list en premier pour résoudre int <: X <: ⊤, et puis on calcule le type de x => x + 1 avec la connaissance int <: X <: ⊤ a priori, malheureusement ça ne résoud pas le problème: voici encore l'appel:

val result: List[int] = map(x => x + 1, list)

depuis l'annotation de result on peut avoir ⊥ <: Y <: int, et depuis list on a int <: X <: ⊤, maintenant on a deux problèmes: d'abord, on ne peut pas typecheck x + 1 parce que on ne sait que int <: X, et pour que x + 1 soit légal il faut que X <: int. Ensuite, même si l'on ignore ce problème et procède, on a deux inégalités ⊥ <: Y <: int et int <: X <: ⊤, normalement on choisit la résolution la plus petite donc ici on devrait choisir Y = ⊥, mais c'est absurde! Maintenant on a x => x + 1: X -> ⊥.

Cas 2e

Bien, alors quand on fait face à ces cas (les arguments dont le typecheck dépend sur d'autres arguments), on peut délibérément le maximiser au lieu de minimiser, mais c'est pas d'abord aussi, voici le programme

val result = map(x => x + 1, list)

c'est prèsque le même programme sauf que result n'est pas annoté, encore on a int <: X <: ⊤, mais maintenant on ne peut collecter aucune information sur Y, même si l'on considère le type de x + 1 et ajoute l'inégalité int <: Y <: ⊤ depuis ça. Selon notre discussion, il faut minimiser x => x + 1: X -> Y et maximiser result: List[Y], mais puisque Y apparaît co- et contravariantement dans le type de x => x + 1 et result, ça nous dit qu'il faut "minimiser" Y en maximisant Y, ce qui est clarement impossible.

Quel est le problème fondamental ici? Qui a causé ça? On a deux observation.

1. Sur le cas 1e, la raison de minimiser Y nous donne ⊥ devrait être grâce au fait que le constraint, ou l'inégalité de Y est calculé depuis l'annotation de result, au lieu de typecheck l'expression x => x + 1 lui-même, ça nous explique pourquoi faisant couler l'information typage depuis le deuxième argument list au premier argument x => x + 1 ne marchera pas.

2. Surl le cas 2e, c'est parce que le deuxième argument x => x + 1 n'est pas typé sur son paramètre x!. D'abord, puisque x est typé, on ne performe pas l'inférence sur x: int => x + 1, le typecheck procédera et nous donne même ⊥ <: X <: int (puisque X apparaît contravariantement à x), int <: Y <: ⊤[1^], et cette fois x: int => x + 1 peut être typé directement, on minimise son type au lieu de le maximiser (c'est important), donc en minimisant à la fois tous ces inégalités, on a X = int (remarquer que X apparaît contravariantement dans le type de x: int => x + 1, donc minimisant X -> Y revient à maximiser X) et Y = int, bingo.

Si l'on regarde à ce problème plus profondément, comment peut-on éviter ce problème et par ailleurs améliorer notre algorithme? La méthode, c'est implement d'annoter x! Dans les deux observations ci-dessus, annotant x nous permet de calculer le type de x + 1, i.e. une borne inférieure de Y en typecheck x + 1 elle-même, et ça fait disappraître le choix entre maximisation et minimisation. Remarquer que si l'argument de x => x + 1 n'est pas typé, il faut unifier X, ce qui est le type de x, avec int, ce qui est un type depuis un endroit plus haut dans l'AST parce qu'on ne peut pas calculer x: int en typecheck l'expression x => x + 1 elle-même, donc il faut venir d'autres entroits, par exemple en typecheck le deuxième argument, ça a caractérisé ce problème, et dans l'article de Odersky, il exige qu'on peut unifier un variable typage T avec un type concret A si et seulement si A est calculé quelque part plus bas dans l'AST.

Quelle est l'approache d'Odersky

Dans l'algorithme de Pierce & Turner, le typecheck est séparé en deux pieces: le check mode et le synthesize mode, et on a un concept de "type de contexte", c'est le type qui est "expecté" d'une expression, dans le paragraphe ci-dessus on a pointé le problème réel ici, maintenant Odersky a figuré une méthode pour résoudre ce problème, lors de préserver une formulation rigoureuse, il a crée, la Colored Local Type Inference, le raffinement le plus notable de cette inférence est de permettre de faire couler l'information typage partielle, dans ce cadre l'expression

où

devient typable, parce qu'on peut utiliser l'information partielle $\tt int \to X$. Dans le paragraph ci-dessus on a déjà su que $\tt int$ est obligatoire ici, alors on fait attention à distinguer les types partiels qui peuvent être utilisés et ceux qui ne le peuvent pas. Cet algorithme sépare tous les types en deux catégories, syntesized ou inherited, ceux qui corrèspondent à le synthesize mode et le check mode dans le système de Pierce & Turner, par défaut, il y a deux règles importants:

1. Tous les variables typages sont inherited pendant l'instantiation.
2. On peut instancier un variable typage X avec un type concret A si et seulement si A est synthesized

int -> X est légal parce que dans ce type on va remplacer X, mais X est à la position covariante, donc lors de remplacer X par int, int est calculé en typecheck l'expression x + 1, il est alors synthesized et éligible pour l'instantiation de X. Mais si $\tt g: \forall X. (X\to X) \to X$, la remplacement ne pourra pas procéder, car il faut remplace le X contravariant avec int, selon le règle du système d'Odersky, le type d'un appel non typé est toujours inherited, donc int ici est aussi un type inherited, par conséquent, l'unification ne marche pas parce qu'on vient d'essayer d'unifier un variable typage T avec un type inherited int.

Un petit détour: La décidablité d'inférence du System F Sub.

  L'inférence du System F n'est pas décidable, tout le monde le sait. Mais au moins son typecheck est décidable. Pour System F Sub, on a même moins d'espoir: pour des certains algorithmes, les subtyping n'est pas décidable, il y a des certains constructions qui va rendre l'algorithme "loop forever". Et plus mauvais: System F Sub peut simuler le Turing Machine (Pour la démonstration, consultez TAPL chapitre 28), et le plus mauvais: si ton langage utilise un système sous-typage nominal, il est undécidable, Le Microsoft a même écrit un article pour ça (et encore une fois les auteurs incluent Benjamin Pierce.). Alors tu peux vois System S Sub n'est pas un système assez bienveillant, mais il est utile, hmmm...
  Dans notre article prochain on verra que le typeclass évite les undécidabilités de System F Sub en ne utilisant pas le sous-typage dans le système.

  事情的起因是这样的，我在我的 Windows 平台上写了一个 Rust 项目，然后我需要把他部署到一个 linux 服务器上，这看上去是一件很稀松平常的事情，于是我先去搜索了 Rust 的交叉编译方法，官方文档里写的很清楚：

$ rustup target add arm-linux-androideabi
info: downloading component 'rust-std' for 'arm-linux-androideabi'
info: installing component 'rust-std' for 'arm-linux-androideabi'

看上去简单的一，先给 rustup 添加一个 target 然后编译的时候指定 target 就行了，于是我去我的 linux 平台跑一个

$ rustup target list | grep "installed"
x86_64-unknown-linux-gnu (installed)

好，现在知道我的 target 是什么了，接下来只需要去执行以下 rustup target add x86_64-unknown-linux-gnu 然后 cargo build --target x86_64-unknown-linux-gnu --release 就完事了，然而调用这个命令的时候出了一个巨长无比的错误，核心思想是这样的：

  Could not find openssl via pkg-config:
  pkg-config has not been configured to support cross-compilation.

  Install a sysroot for the target platform and configure it via
  PKG_CONFIG_SYSROOT_DIR and PKG_CONFIG_PATH, or install a
  cross-compiling wrapper for pkg-config and set it via
  PKG_CONFIG environment variable.

  cargo:warning=Could not find directory of OpenSSL installation, and this `-sys` crate cannot proceed without this knowledge. If OpenSSL is installed and this crate had trouble finding it,  you can set the `OPENSSL_DIR` environment variable for the compilation process. See stderr section below for further information.

这就很几把扯淡了，意思是我需要安装 openssl 和 pkg-config，问题这俩在 Windows 上肯定是装不了的，没办法，那试试 WSL 吧，我在 WSL 上确认了 openssl 和 pkg-config 都安装好了，然后重复上面的步骤，ok，编译好了，给我乐的，马上上传到我自己的 ubuntu 服务器上写了个服务准备跑起来。
然后我就释然了，沟槽的 WSL 编译的 glibc 和 ubuntu 编译的 glibc 版本不一样。踏马的服务器上要 glibc 2.32，然后鬼知道 WSL 编译时候用的哪个版本的 glibc，行吧，那我再去找找怎么在编译的时候指定 glibc 版本，后来说实在不行自己在目标机上编译一份 glibc 吧，半个小时框框框编译完了，嘿，您才怎么着，不成，编译的时候没法他妈的指定 glibc 版本，要么他妈的换个 glibc 版本一致的 linux distro，要么就用 docker 去，问题我上哪重装 linux 去？docker 更是压根不想用，没办法，继续找，找到有人说可以用 musl 静态编译代替 glibc 动态链接，成，再试试。OK，又回来了，openssl 和 pkg-config 找不到的错误又几把回来了，我就寻思这到底是怎么个JB事，musl 不行再试试 zigbuild 吧，一模一样的狗屎错误，我又仔细看了一眼错误日志，发现设置 OPENSSL_DIR，OPENSSL_LIB_DIR，和 OPENSSL_INCLUDE_DIR 这几个环境变量也成，可能是虽然装了 libssl-dev 但是环境变量没指定，ok，接下来去 dpkg 一下 libssl-dev 的安装位置，跑一下 dpkg -L libssl-dev，输出了巨长一串

/.
/usr
/usr/include
/usr/include/openssl
/usr/include/openssl/aes.h
/usr/include/openssl/asn1.h
/usr/include/openssl/asn1_mac.h
/usr/include/openssl/asn1err.h
/usr/include/openssl/asn1t.h
/usr/include/openssl/async.h
/usr/include/openssl/asyncerr.h
/usr/include/openssl/bio.h
/usr/include/openssl/bioerr.h
/usr/include/openssl/blowfish.h
/usr/include/openssl/bn.h
/usr/include/openssl/bnerr.h
/usr/include/openssl/buffer.h
/usr/include/openssl/buffererr.h
/usr/include/openssl/camellia.h
/usr/include/openssl/cast.h
/usr/include/openssl/cmac.h
/usr/include/openssl/cmp.h
/usr/include/openssl/cmp_util.h
/usr/include/openssl/cmperr.h
/usr/include/openssl/cms.h
/usr/include/openssl/cmserr.h
/usr/include/openssl/comp.h
/usr/include/openssl/comperr.h
/usr/include/openssl/conf.h
/usr/include/openssl/conf_api.h
/usr/include/openssl/conferr.h
/usr/include/openssl/conftypes.h
/usr/include/openssl/core.h
/usr/include/openssl/core_dispatch.h
/usr/include/openssl/core_names.h
/usr/include/openssl/core_object.h
/usr/include/openssl/crmf.h
/usr/include/openssl/crmferr.h
/usr/include/openssl/crypto.h
/usr/include/openssl/cryptoerr.h
/usr/include/openssl/cryptoerr_legacy.h
/usr/include/openssl/ct.h
/usr/include/openssl/cterr.h
/usr/include/openssl/decoder.h
/usr/include/openssl/decodererr.h
/usr/include/openssl/des.h
/usr/include/openssl/dh.h
/usr/include/openssl/dherr.h
/usr/include/openssl/dsa.h
/usr/include/openssl/dsaerr.h
/usr/include/openssl/dtls1.h
/usr/include/openssl/e_os2.h
/usr/include/openssl/ebcdic.h
/usr/include/openssl/ec.h
/usr/include/openssl/ecdh.h
/usr/include/openssl/ecdsa.h
/usr/include/openssl/ecerr.h
/usr/include/openssl/encoder.h
/usr/include/openssl/encodererr.h
/usr/include/openssl/engine.h
/usr/include/openssl/engineerr.h
/usr/include/openssl/err.h
/usr/include/openssl/ess.h
/usr/include/openssl/esserr.h
/usr/include/openssl/evp.h
/usr/include/openssl/evperr.h
/usr/include/openssl/fips_names.h
/usr/include/openssl/fipskey.h
/usr/include/openssl/hmac.h
/usr/include/openssl/http.h
/usr/include/openssl/httperr.h
/usr/include/openssl/idea.h
/usr/include/openssl/kdf.h
/usr/include/openssl/kdferr.h
/usr/include/openssl/lhash.h
/usr/include/openssl/macros.h
/usr/include/openssl/md2.h
/usr/include/openssl/md4.h
/usr/include/openssl/md5.h
/usr/include/openssl/mdc2.h
/usr/include/openssl/modes.h
/usr/include/openssl/obj_mac.h
/usr/include/openssl/objects.h
/usr/include/openssl/objectserr.h
/usr/include/openssl/ocsp.h
/usr/include/openssl/ocsperr.h
/usr/include/openssl/opensslv.h
/usr/include/openssl/ossl_typ.h
/usr/include/openssl/param_build.h
/usr/include/openssl/params.h
/usr/include/openssl/pem.h
/usr/include/openssl/pem2.h
/usr/include/openssl/pemerr.h
/usr/include/openssl/pkcs12.h
/usr/include/openssl/pkcs12err.h
/usr/include/openssl/pkcs7.h
/usr/include/openssl/pkcs7err.h
/usr/include/openssl/prov_ssl.h
/usr/include/openssl/proverr.h
/usr/include/openssl/provider.h
/usr/include/openssl/rand.h
/usr/include/openssl/randerr.h
/usr/include/openssl/rc2.h
/usr/include/openssl/rc4.h
/usr/include/openssl/rc5.h
/usr/include/openssl/ripemd.h
/usr/include/openssl/rsa.h
/usr/include/openssl/rsaerr.h
/usr/include/openssl/safestack.h
/usr/include/openssl/seed.h
/usr/include/openssl/self_test.h
/usr/include/openssl/sha.h
/usr/include/openssl/srp.h
/usr/include/openssl/srtp.h
/usr/include/openssl/ssl.h
/usr/include/openssl/ssl2.h
/usr/include/openssl/ssl3.h
/usr/include/openssl/sslerr.h
/usr/include/openssl/sslerr_legacy.h
/usr/include/openssl/stack.h
/usr/include/openssl/store.h
/usr/include/openssl/storeerr.h
/usr/include/openssl/symhacks.h
/usr/include/openssl/tls1.h
/usr/include/openssl/trace.h
/usr/include/openssl/ts.h
/usr/include/openssl/tserr.h
/usr/include/openssl/txt_db.h
/usr/include/openssl/types.h
/usr/include/openssl/ui.h
/usr/include/openssl/uierr.h
/usr/include/openssl/whrlpool.h
/usr/include/openssl/x509.h
/usr/include/openssl/x509_vfy.h
/usr/include/openssl/x509err.h
/usr/include/openssl/x509v3.h
/usr/include/openssl/x509v3err.h
/usr/include/x86_64-linux-gnu
/usr/include/x86_64-linux-gnu/openssl
/usr/include/x86_64-linux-gnu/openssl/configuration.h
/usr/include/x86_64-linux-gnu/openssl/opensslconf.h
/usr/lib
/usr/lib/x86_64-linux-gnu
/usr/lib/x86_64-linux-gnu/libcrypto.a
/usr/lib/x86_64-linux-gnu/libssl.a
/usr/lib/x86_64-linux-gnu/pkgconfig
/usr/lib/x86_64-linux-gnu/pkgconfig/libcrypto.pc
/usr/lib/x86_64-linux-gnu/pkgconfig/libssl.pc
/usr/lib/x86_64-linux-gnu/pkgconfig/openssl.pc
/usr/share
/usr/share/doc
/usr/share/doc/libssl-dev
/usr/lib/x86_64-linux-gnu/libcrypto.so
/usr/lib/x86_64-linux-gnu/libssl.so
/usr/share/doc/libssl-dev/changelog.Debian.gz
/usr/share/doc/libssl-dev/changelog.gz
/usr/share/doc/libssl-dev/copyright

挺有意思，注意到在 /usr/lib/x86_64-linux-gnu 有一个 libssl.so，大胆猜测一下应该设置到这里，于是尝试设置 OPENSSL_DIR=/usr/lib/x86_64-linux-gnu，再跑一次编译，错误日志提示在 OPENSSL_DIR 下面找不到 include 文件夹，何意味？再看看输出，发现 include 文件夹就只有一个 /usr/include，那行吧，再设置 OPENSSL_DIR 到 /usr/include，继续报错，这次错误日志又变了，提示

  cargo:warning=In file included from build/expando.c:1:
  cargo:warning=In file included from /usr/include/openssl/opensslv.h:109:
  cargo:warning=/usr/include/openssl/macros.h:14:10: fatal error: 'openssl/opensslconf.h' file not found
  cargo:warning=   14 | #include <openssl/opensslconf.h>
  cargo:warning=      |          ^~~~~~~~~~~~~~~~~~~~~~~
  cargo:warning=1 error generated.

合着找不到头文件，继续看上面 dpkg 的输出，发现 opensslconf.h 在 /usr/include/x86_64-linux-gnu/openssl 下面

......

这他妈不对啊，合着这俩文件是分开的，你又要我在 openssl 文件夹里必须有一个 include 文件夹，然后又要求有一个 opensslconf.h 文件，问题这文件所在的 openssl 文件夹里没有 include 文件夹，有 include 文件夹的目录里没有 openssl/opensslconf.h 文件，我的心中和吃了屎一样难受，那现在几把怎么办？只有蒙，大力出奇迹 symlink 一下得了

cd /usr/include/openssl
sudo ln -s ../x86_64-linux-gnu/openssl/configuration.h
sudo ln -s ../x86_64-linux-gnu/openssl/opensslconf.h

把 /usr/include/x86_64-linux-gnu/openssl 下面的文件全部 symlink 到 /usr/include 下面，然后再试这编译一次，我草，居然行了，一人一句 symlink 牛逼来，真他妈编译过了就离谱，我正乐着呢，又几把报错了

  = note: error: unable to find dynamic system library 'pq' using strategy 'no_fallback'. searched paths:
            /tmp/rustcxB9ZPT/raw-dylibs/libpq.so
            /mnt/d/Projects/frederica-backend/target/x86_64-unknown-linux-gnu/debug/build/zstd-sys-1a7aabc5fc036d0f/out/libpq.so
            /usr/lib/x86_64-linux-gnu/libpq.so
            /usr/lib/x86_64-linux-gnu//libpq.so
            /home/dylech30th/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libpq.so

还好这问题大爹我早遇到过了，本质上是和 libssl-dev 一样的问题，开发包和运行包不是同一个，所以我还得再去 apt install libpq-dev，装完之后这个问题就消失了，然后爆了一个巨长无比的 linker 错误

error: linking with `/home/dylech30th/.cache/cargo-zigbuild/0.19.8/zigcc-x86_64-unknown-linux-gnu.2.32-a726.sh` failed: exit status: 1
  |
  = note:  "/home/dylech30th/.cache/cargo-zigbuild/0.19.8/zigcc-x86_64-unknown-linux-gnu.2.32-a726.sh" "-m64" "/tmp/rustcpCTr79/symbols.o" "<257 object files omitted>" "-Wl,--as-needed" "-Wl,-Bstatic" "/mnt/d/Projects/frederica-backend/target/x86_64-unknown-linux-gnu/debug/deps/{libfutures-28d154dcf4417f9d.rlib,libfutures_executor-7afba41877da7d24.rlib,libenv_logger-0f342fc62e053652.rlib,libanstream-ed9255ada3c86e2e.rlib,libanstyle_query-cfb41ab8e4e18588.rlib,libis_terminal_polyfill-bb585aa3271b8f3b.rlib,libcolorchoice-6fc0ea92d9b11814.rlib,libanstyle_parse-29a81a16b35ffd3e.rlib,libutf8parse-74725c6e09e49c5b.rlib,libenv_filter-5fcc9abcfd305c99.rlib,libanstyle-19eec67bac9e098d.rlib,libhumantime-20c091a993b28278.rlib,libactix_cors-ed2bef01fe92880a.rlib,libactix_web_lab-205a20e0be64cf96.rlib,libserde_html_form-458f59eea684a542.rlib,libserde_path_to_error-e3529938f2ecf13e.rlib,libcsv-af94fa7da53d19a1.rlib,libcsv_core-36a775b8ffe0d467.rlib,libtokio_stream-d93e6cdc3a0a0c3d.rlib,libarc_swap-04b9e0e241faa2f1.rlib,libitertools-c62a2bba330c6f0f.rlib,librayon-1fa94b843f65454b.rlib,librayon_core-945d539473b0ebe5.rlib,libcrossbeam_deque-d3031ad376af31d0.rlib,libcrossbeam_epoch-1d6047a65fde79c1.rlib,libcrossbeam_utils-8d311c0411b41b60.rlib,libeither-f8ce232013b046e8.rlib,libdotenvy-ee87299280fbc5fd.rlib,libopenai-40f8ee9bc42795fc.rlib,libderive_builder-1d7303fbbce25113.rlib,libreqwest_eventsource-418678404d8c1635.rlib,libfutures_timer-72451361586a40a8.rlib,libeventsource_stream-55b6a2015740818f.rlib,libnom-3b980d2e6a245a33.rlib,libthiserror-6087a7caacad2188.rlib,libreqwest-f7116e5c16a70ee4.rlib,librustls_pemfile-6a273cf6618a1bc6.rlib,librustls_pki_types-38e6110c0f393cda.rlib,libipnet-497f3e06a1108483.rlib,libhyper_tls-75c1fbba90062675.rlib,libtokio_native_tls-0b979e811882bfdd.rlib,libmime_guess-44321fe1135443be.rlib,libunicase-0f8d564370bb92ce.rlib,libtower-18209f827463969d.rlib,libsync_wrapper-c689a8c1f665c4c9.rlib,libtower_layer-c2674b9da58a4d13.rlib,libnative_tls-39174f8310abbd7a.rlib,libopenssl_probe-8ef84cb165b0ef19.rlib,libopenssl-912d6f09ec6e85ac.rlib,libforeign_types-087fedfa4d20c1c9.rlib,libforeign_types_shared-6efe75ea064be7de.rlib,libopenssl_sys-a4b8cd594b862840.rlib,libhyper_util-484cdf3dbce83dde.rlib,libtower_service-322dd60aed3b1dea.rlib,libhyper-e738a3c263318afa.rlib,libwant-5b440e7d6088f80f.rlib,libtry_lock-34b02f6f3478429e.rlib,libhttp_body_util-cf8ea1df72e64977.rlib,libhttp_body-45d773453add52ba.rlib,libhttp-9dc288d78e14873a.rlib,libdiesel-cf5062fa1e2699c6.rlib,libpq_sys-84e99b69fc8e7af2.rlib,libchrono-4f82d3d4d7fe405a.rlib,libnum_traits-63dd1f13f8b5c3b0.rlib,libiana_time_zone-22cabdfb2a11fda0.rlib,libactix_session-e5c58bdf5eca194d.rlib,libanyhow-30592129842efc8f.rlib,libderive_more-5c4686c2aaf9c616.rlib,libactix_web-639ecdfddf900af9.rlib,libimpl_more-da3ed08da16e6c9b.rlib,libahash-7a59c16e05f8ed6a.rlib,liburl-4654215b5c6eb9fd.rlib,libidna-b14b7bb1a90550e0.rlib,libidna_adapter-8a7d2a624ab2f8c3.rlib,libicu_normalizer-04ec792676924b86.rlib,libicu_normalizer_data-0d90e535bedb5b17.rlib,libwrite16-db7f68fc5b72350a.rlib,libutf8_iter-ccfb3617fc4fa9f4.rlib,libutf16_iter-86733479d1733101.rlib,libicu_properties-6bc01a97ef6de707.rlib,libicu_properties_data-2d8ac5a423c19d2a.rlib,libicu_locid_transform-d4dd757ae144cc49.rlib,libicu_locid_transform_data-915cc8cb8bf7c395.rlib,libicu_collections-4b07ba87da47450f.rlib,libicu_provider-fa8d6ab14c3ee82d.rlib,libicu_locid-a3c903f868b30b4e.rlib,liblitemap-cccb2c2541472698.rlib,libtinystr-0720842c88ad91e3.rlib,libzerovec-8ee2beb5f8259ada.rlib,libwriteable-7e3bf3e3ae5c261b.rlib,libyoke-54dfcc9648ce4399.rlib,libzerofrom-cf4930045c2af940.rlib,libstable_deref_trait-8a76cab77ef9c922.rlib,libserde_urlencoded-2419948425a213c7.rlib,libform_urlencoded-908b20cfc525577b.rlib,libserde_json-a67c450216ffcebb.rlib,libryu-6b97a2af8b61c3aa.rlib,libactix_server-224f46475f3f558b.rlib,libactix_router-efe6dbe587c2fd98.rlib,libregex-baada6241b36f2a0.rlib,libregex_automata-1b4c5170ef354950.rlib,libaho_corasick-5060936f61189976.rlib,libregex_syntax-2c95a15ec4bf9be7.rlib,libserde-58998fc25b7ec277.rlib,libcookie-a3283456a5ecf68e.rlib,libhkdf-99783cb6c9e6ebed.rlib,libhmac-d29e0c9a474a5e48.rlib,libsha2-63ed8b3250d44dca.rlib,libtime-6ab592201f9b3509.rlib,libtime_core-926a686092f4ddf0.rlib,libnum_conv-4f02ec588889a7cd.rlib,libderanged-85ce092712131791.rlib,libpowerfmt-c1003d41801b8940.rlib,libaes_gcm-abcdcf16b5a8391d.rlib,libctr-78854c90719b9013.rlib,libghash-474b6e46aba177eb.rlib,libpolyval-b6c2d8df0d105a69.rlib,libopaque_debug-be73cc5f3e239007.rlib,libuniversal_hash-4062c9e6df99e290.rlib,libaes-8d954c81e282f039.rlib,libcipher-aaa71d49668fe95c.rlib,libinout-91ab31f48f675584.rlib,libaead-15d4c2a8a283ee50.rlib,libbase64-9596453e5d408d0d.rlib,librand-fb1eae64ed67690e.rlib,librand_chacha-336df4caa6f387f5.rlib,libactix_http-12bd4f8466d999c2.rlib,librand-fa0dd7b3140f3748.rlib,librand_chacha-fb35aca615b714c4.rlib,libppv_lite86-ac7a74c674f7665c.rlib,libzerocopy-b1450fec840c68df.rlib,libbyteorder-19d23b0c1f352eee.rlib,libzerocopy-932b1d057b6466de.rlib,librand_core-6e2937d5e0bfab56.rlib,libgetrandom-fc08723758f9be23.rlib,libhttparse-855df5f56dc698f1.rlib,libbrotli-f7261692615a72ce.rlib,libbrotli_decompressor-9a2fdb7d7bf4e19b.rlib,liballoc_stdlib-80b9089404efdf9e.rlib,liballoc_no_stdlib-e4d6bbb171ded188.rlib,libhttpdate-f364a73698e48e2f.rlib,libsha1-81bdfbb24aed0850.rlib,libcpufeatures-ece78655b26f4a05.rlib,libdigest-a6b4c631e853691d.rlib,libsubtle-30af2ac99eb21e63.rlib,libblock_buffer-a431b58371fdce6b.rlib,libcrypto_common-d285f07457f7cd19.rlib,libgeneric_array-413a674fd41188ca.rlib,libtypenum-70db351557104c52.rlib,librand_core-98af2d5f4edb37ad.rlib,libgetrandom-c363aec5b34ab3a2.rlib,libbase64-50bb4bd7752c9e50.rlib,liblocal_channel-2636115450af4df2.rlib,libbytestring-170fbbbd15a54a18.rlib,libencoding_rs-004ad421b322ee45.rlib,liblanguage_tags-a19f35e61c427022.rlib,libfoldhash-9cf1be45d6d20405.rlib,libmime-c3542cde661420ef.rlib,libpercent_encoding-5a27c142a4b5af60.rlib,libh2-e63266216982e3e6.rlib,libindexmap-6f4c4ec2b63b4fc8.rlib,libequivalent-8ed4c122ac6c3754.rlib,libhashbrown-3138d022f535c54d.rlib,libfutures_util-ff503660ed976e0d.rlib,libfutures_io-f7841a1d4b2c8784.rlib,libslab-046a8c499d9f672b.rlib,libfutures_channel-298679a65aa5d402.rlib,libfutures_task-1882f3776cdef32e.rlib,libpin_utils-3d9c084ce0305a4f.rlib,libzstd-ea92576b8634ab5f.rlib,libzstd_safe-2552d686dd48810a.rlib,libzstd_sys-01f74130c0e1533c.rlib,libflate2-53facf83b3168818.rlib,libminiz_oxide-b4bf5c84fe5c7f82.rlib,libadler2-953fe117f84d7ece.rlib,libcrc32fast-098a477913947e23.rlib,libactix_service-d140a2d464f8a1a4.rlib,libactix_codec-710d54ccde03656a.rlib,libtracing-a83c9a1a1f8b9409.rlib,libtracing_core-9f1f646e757746b1.rlib,libonce_cell-f0dab71049208f9e.rlib,libmemchr-7ec3bcdaedc57676.rlib,libbitflags-ff225e8bf7c36bb4.rlib,libtokio_util-15a6231dbfa60593.rlib,libfutures_sink-86dbd95a0a0a11d9.rlib,libderive_more-b886cc716046e66d.rlib,libactix_utils-dd761ede39dabe08.rlib,liblocal_waker-a92283d6afd83527.rlib,libactix_rt-c43b9b746cf118cc.rlib,libtokio-aebcbae84aa6f4d5.rlib,libsignal_hook_registry-69b9a637fdad229b.rlib,libsocket2-c9b4c3b1d30da451.rlib,libmio-0469516820ff45cc.rlib,liblog-f9cfc06303bbc794.rlib,libparking_lot-9b3ac4e065aa65cf.rlib,libparking_lot_core-241955c5acb0a916.rlib,liblibc-65ace88b122d3ed2.rlib,libcfg_if-f090c1b66e80a751.rlib,libsmallvec-d929178cf6e55e7d.rlib,liblock_api-e8c9adc9599db8b4.rlib,libscopeguard-e7374d89a87a1c19.rlib,libpin_project_lite-6be4057f176e8b62.rlib,libfutures_core-cadb133a0b7579af.rlib,libhttp-e8eb530446d168cf.rlib,libitoa-5e2bc39ac7c972db.rlib,libbytes-653b9fb69aa77a44.rlib,libfnv-30db6334de191cc9.rlib}.rlib" "<sysroot>/lib/rustlib/x86_64-unknown-linux-gnu/lib/{libstd-*,libpanic_unwind-*,libobject-*,libmemchr-*,libaddr2line-*,libgimli-*,librustc_demangle-*,libstd_detect-*,libhashbrown-*,librustc_std_workspace_alloc-*,libminiz_oxide-*,libadler2-*,libunwind-*,libcfg_if-*,liblibc-*,liballoc-*,librustc_std_workspace_core-*,libcore-*,libcompiler_builtins-*}.rlib" "-Wl,-Bdynamic" "-lssl" "-lcrypto" "-lpq" "-lgcc_s" "-lutil" "-lrt" "-lpthread" "-lm" "-ldl" "-lc" "-L" "/tmp/rustcpCTr79/raw-dylibs" "-B<sysroot>/lib/rustlib/x86_64-unknown-linux-gnu/bin/gcc-ld" "-fuse-ld=lld" "-Wl,-znostart-stop-gc" "-Wl,--eh-frame-hdr" "-Wl,-z,noexecstack" "-L" "/mnt/d/Projects/frederica-backend/target/x86_64-unknown-linux-gnu/debug/build/zstd-sys-a4a188e3287a6347/out" "-L" "/usr/lib/x86_64-linux-gnu" "-L" "/usr/lib/x86_64-linux-gnu/" "-L" "<sysroot>/lib/rustlib/x86_64-unknown-linux-gnu/lib" "-o" "/mnt/d/Projects/frederica-backend/target/x86_64-unknown-linux-gnu/debug/deps/frederica_backend-728b5dfb69f05063" "-Wl,--gc-sections" "-pie" "-Wl,-z,relro,-z,now" "-nodefaultlibs"
  = note: some arguments are omitted. use `--verbose` to show all linker arguments
  = note: error: unsupported linker extension flag: -z nostart-stop-gc


warning: `frederica-backend` (bin "frederica-backend") generated 24 warnings
error: could not compile `frederica-backend` (bin "frederica-backend") due to 1 previous error; 24 warnings emitted

看得懂不？看不懂吧，我也看不懂，好在这问题 google 一下就有人发现一个星期前提到过，只需要设置一个 rust 编译的环境变量

export RUSTFLAGS="-Zlinker-features=-lld"

就 OK 了，看了一下，也没看明白 -lld 之后 rust 会用哪个 linker，但是总之是成了。

总结一下

总结一下，解决这个问题的流程，首先是不要走 Windows 交叉编译，去 WSL 编译，同时弄明白编译时候的 glibc 版本是什么，然后用 zigbuild 或者 musl 去编译，这俩一个是允许你设定 glibc 版本，一个是可以静态编译不走动态链接，接下来，他妈的他编译时候用的 openssl 的目录和环境变量完全是扯JB蛋，首先设置三个环境变量

OPENSSL_INCLUDE_DIR=/usr/include
OPENSSL_DIR=/usr/include
OPENSSL_LIB_DIR=/usr/lib/x86_64-linux-gnu/

OPENSSL_LIB_DIR 根据你发行版不同这个是可能会变的，记得去根据你的实际目录名去选择，接下来再设置一下 symlink，把 /usr/lib/x86_64-linux-gnu/openssl 下面的两个头文件软链接到 /usr/include 下面

cd /usr/include/openssl
sudo ln -s ../x86_64-linux-gnu/openssl/configuration.h
sudo ln -s ../x86_64-linux-gnu/openssl/opensslconf.h

最后，如果你用了类似 ORM 的框架，一定记得安装对应 ORM 框架的开发包，比如在这里要

apt install libpq-dev

然后接着切换 linker

export RUSTFLAGS="-Zlinker-features=-lld"

到了这个时候，再去调用 zigbuild 构建

cargo zigbuild --target x86_64-unknown-linux-gnu.2.32 --release

这里的 2.32 是你目标机需求的 glibc 版本，当然，如果你选择了 musl 就没必要这么做，详见这里的第一条回答。

然后你就终于可以抱着吃了屎一样的心情运行起来了，珍爱生命，远离交叉编译

套盾：本文用到的英文术语皆是本人实在不知道如何翻译、觉得翻译过来意思实在是不对、或者干脆是觉得翻译过来理解起来比不翻译更麻烦（例如“结构归纳法是对良基归纳法的一个实例化”这种句子放在中文里实在是有些狗屁不通了），不是为了故意装逼，这些术语都可以在 Wikipedia 上查到。

  在上一个章节中，我讲到了对归纳法的 generalization，即证明 Principle of Induction 蕴含了常见的数学归纳法，既然是对数学归纳法的一种 generalization，我们也可以轻易的将 Principe of Induction 中的 $\mu F$ 设定为除了 $\N$ 以外的其他归纳集合（例如可以将某个递归数据结构的所有层级作为 $\mu F$，我们就得到了 structural induction），不仅如此，通过取 Principle of Induction 的对偶，我们同样可以得到 Principle of Coinduction。令 $F:\mathcal{P}(U)\rightarrow \mathcal{P}(U)$，注意到在上一篇文章中提到了 $\mu F$ 是 $F$ 的最小不动点，而最小不动点对应 Principle of Induction，很容易就可以发现 $\mu F$ 实际上包含了所有可以由递归的应用 $F$ 得到的有限大的数据，以 $U=\N$ 为例，定义 $F: \mathcal{P}(\N)\rightarrow \mathcal{P}(\N) := X\mapsto \lbrace 0\rbrace \cup \lbrace x + 1\ |\ x\in X\rbrace$，则显然 $\mu F=\N$，也即所有有限大的自然数集合（当然了，没有无限大的自然数，除非我们对自然数集进行一些扩充，在此仅仅是举一个例子）：首先，$\N$ 是一个 $F$-closed 集合，所以 $\mu F\subseteq \N$；其次，我们用归纳法证明 $\forall n\in \N. n\in\mu F$，也即 $\N\subseteq \mu F$：首先，$0$ 显然属于 $\mu F$，其次由不动点的定义，有 $F(\mu F)=\mu F$，因为 $F(\mu F)= \lbrace 0\rbrace \cup \lbrace x + 1\ |\ x\in \mu F\rbrace$，如果 $n\in\mu F$，则显然 $n+1\in F(\mu F)=\mu F$，也即 $n+1\in \mu F$。以上论证适用于各种归纳定义得到的结构，例如读者可以轻松发现，如果将 $\N$ 换成 $\sf list = nil\ |\ cons(\mathrm{\Sigma}, list)$，其中 $\Sigma$ 是任意一个字母表，上面的论证一样成立。如果使用一些更加抽象的设定，我们应该可以证明该属性不仅仅是对 $\N$ 或 $\sf list$，而是对所有 inductive set 都成立，只是笔者才疏学浅，加上这部分内容超出了本文的主旨，因此不再就具体如何证明加一赘述，而仅仅给出一个思路供参考：

一种“更抽象的设定”可以由如下的思路给出：每个 inductive set $I$ 都可以被一组 inference rules 所唯一确定（uniquely determined），因此，我们可以选择不去吧 $I$ 想象成一个具体数学对象的集合，而是想象成一个由这些 inference rules 的 derivation tree 所构成的集合，每一个 derivation tree 唯一的对应着其所 derive 出的数学对象，比如在 $\N$ 中，$3$ 可以对应如下的 derivation tree：

$$
\cfrac{\cfrac{\cfrac{\cfrac{}{0}}{0+1}}{0+1+1}}{0+1+1+1}
$$

通过这种办法，我们将所有 inductive set 中的每个元素都变成了一个树状的结构，此时，我们可以用一个函数 $T(s)$ 来编码这个树，具体方法如下：假设这颗 derivation tree 至多有 $n$ 个分支，那么令 $s=\lbrace 1, ..., N \rbrace^{\ast}$ 是一个由从 1 到 $N$ 的数字构成的字符串，其逻辑是 T(s) 会返回 derivation tree 中的某个节点，令 $\epsilon$ 是空字符串，则 $T(\epsilon)$ 为跟节点，而如果 $s\neq \epsilon$，则 $s$ 中的每个数字告诉了选择当前节点从左往右数的第几个子节点，例如，令 $s=121$，这意味这选择根节点的第一个子节点的第二个子节点的第一个子节点，通过这种方法，我们可以用 $T(s)$ 来编码任意的 derivation tree，又因为 $T(s)$ 唯一的特征就是 $s$，我们也就实现了一个用字符串 $s=\lbrace 1, ..., N \rbrace^{\ast}$ 来编码任意 inductive set 的任意元素的方法（注意，这也意味着可能存在不同 inductive set 的不同元素有着相同的特征字符串 $s$ 的可能，但是这不要紧，因为我们只关注这样的一个元素是否是有限大的，而这是由 inference rules 的层数是否有限，也即 $s$ 的长度是否有限决定的，与元素本身以及 derive 出该元素的 inference rules 究竟长什么样子没有关系），此时，通过对 $s$ 的长度做归纳即可进行证明。

因为 $\mu F$ 对应所有有限大的结构，因此与 $\mu F$ 相关联的 Principle of Induction 自然也就告诉了如何论证有关所有有限大 ¹的结构的命题。相对应的，通过对 Principle of Induction 中的所有内容取对偶，我们就得到了 Principle of Coinduction，通过取对偶，不难得知 $F$ 的最大不动点 $\nu F$ 对应了所有有限大以及无限大的结构，而与 $\nu F$ 相关的 Principle of Coinduction 告诉了我们如何论证有关任意无限大的结构的命题。
  一个自然的落入 Coinduction 范畴的例子是 $\sf Stream$，在很多编程语言中，也叫做 infinite list 或者 lazy list，$\sf Stream$ 对应一个无限的数据列表。我们都知道 $\sf list$ 是一个 Inductive Type，不难发现，对于 $\sf list$ 来说，我们可以通过重复组合 $\sf nil$ 和 $\sf cons$ 来一步一步构建出任何 $\sf list$；但是对于 $\sf Stream$ 来说，由于所有 $\sf Stream$ 默认都是无限大的，我们不可能能想办法去构造一个 $\sf Stream$，我们所能做到的，仅仅是观察一下这个 $\sf Stream$ 的头部是什么元素，也就是说，$\sf Stream$ 会包含两个操作，$\sf head$ 和 $\sf tail$，其中 $\sf head$ 返回一个 $\sf Stream$ 的头部元素，而 $\sf tail$ 返回 $\sf Stream$ 去掉头部元素的剩余部分，也即一个新的无限的数据列表，不难发现，与 $\sf list$ 的 $\sf nil$ 以及 $\sf cons$ 都是用于构造的 constructor 不同，一个无限大的 $\sf Stream$ 只能拥有 destructor $\sf head$ 和 $\sf tail$，这样的一个类型就叫做一个 Coinductive Type。
  对于 Inductive Type，我们使用递归函数来分解它，例如，对于一个 $\sf len(list)$，其定义大概率将会是

$$
\begin{aligned}
\sf len(nil) &= 0
\end{aligned}
$$

$$
\sf len(cons(\pi, \tau)) = 1 + \sf len(\tau)
$$

这样的一个算法非常典型的展示了我们是如何使用递归来处理一个 Inductive Type 的，类似的，对于 Coinductive，我们也需要 Corecursion 来处理 Coinductive Type，与 Coinduction 一样，Corecursion 是通过对普通的递归取对偶得到的，普通的递归通过分解 Inductive Type 来分析它，Corecursion 则反过来，从头开始构建一个 Coinductive Type 的实例，例如在 C# 中，IEnumerable<T> 可以被看做是一个 Coinductive Type，而一个典型的 Corecursion 算法就是使用 yield 的斐波那契数列生成器：

public static IEnumerable<int> Fib() {
    var a = 0;
    var b = 1;
    while (true) {
        yield return a;
        (a, b) = (b, a + b);
    }
}

注意到在这样的一个算法是如何生成一个 Coinductive Type IEnumerable<int> 的。
  值得一提的是，Inductive Type 和 Coinductive Type 这一组对偶的概念并非完全对立，一个函数 $F: X\times A\rightarrow X$ 可以被看做是一个 Inductive Type 的生成函数，例如，如果取 $X=\sf list$，$A=\N$，令

$$
F(list, n) = \mathsf{cons}(n, list)
$$

则 $F$ 显然是一个 $\sf list$ 的生成函数，这个函数的签名 $X\times A\rightarrow X$ 告诉我们，给出一个 Inductive Type 的结构 $x: X$，和一个新的元素 $a: A$，会返回一个将 $a$ 与 $x$ 按照 $X$ 的 constructor 结合起来的新的 $X$。但是，如果我们将 $F$ 柯里化，就得到了 $F: X \rightarrow A\rightarrow X$，或者说 $F: X\rightarrow (A\rightarrow X)$，则 $F$ 又可以看做是一个 Coinductive Type 的 observer，其中 $X$ 是初始的值，而 $A$ 代表当前的状态，或者迭代的次数（例如上文 Fib 函数中的 a 和 b 变量就是状态变量），而 $A\rightarrow X$ 是一个状态转移函数，告诉我们在某个特定的输入 $A$，会产出什么样、或者说观察到什么样的 $X$（例如 Fib 函数中根据当前的状态 a 和 b 产出 $X$ 中对应的下一个元素 a + b），这告诉了我们某些函数既可以被当做是 Inductive Type 上的操作（我们说这样的操作是 algebraic 的），也可以被当作是 Coinductive Type 上的操作（我们说这样的操作是 coalgebraic 的），不难发现，algebraic operation 与 coalgebraic operation 的区别就在于一个在表现上是 construction，而另一个则在表现上是 destruction/observation：通过取出 $X$ 的第一个元素来观察 $X$ 的内容。对于了解状态机的人，可以在这里将 $X$ 想象作状态空间，而将 $A$ 想象成状态机的字母表。

  在本篇文章中，我们解释了 Induction 为什么能够论证和构造有限大的数据，而 Coinduction 为什么能够论证和构造无限大的数据。在本系列的下一篇文章中，我们将会介绍 Induction 与 Coinduction 在证明技巧上的区别。

套盾：本文用到的英文术语皆是本人实在不知道如何翻译、觉得翻译过来意思实在是不对、或者干脆是觉得翻译过来理解起来比不翻译更麻烦（例如“结构归纳法是对良基归纳法的一个实例化”这种句子放在中文里实在是有些狗屁不通了），不是为了故意装逼，这些术语都可以在 Wikipedia 上查到。

  在2021年最开始看 Types and Programming Languages 的时候，前面一直看的都非常顺利，结果到了 Recursive Type 对应的章节直接傻了眼，由于缺乏相关内容的熟练度，再加上个人感觉这一章设计的着实不是太好，结果导致我根本没看懂。前几天在南京和朋友讨论逻辑的时候突然想起来了这么一茬，决定把当时整理的笔记发出来，顺便把书里书外的内容都整理的更清楚一些。

  要了解如何 reasoning about 有限以及无限的内容，我们至少需要知道什么是归纳，与高中学习到的不同，归纳法不仅可以应用在自然数上，而是可以应用在任何 well-founded 的关系上，其中一个例子是 structural induction，我们可以认为 structural induction 是对 well-founded induction 的一个 instantiation，其中某个节点和它的 immediate substructure 构成了一个 well-founded relation，因此我们可以对一个树状或者图状的任何拥有一些拓扑意义上的序的结构进行归纳论证。
  几个自然而然的问题是：为什么归纳能行？为什么归纳是正确的？我们能对归纳法本身做些什么 generalization？

为什么归纳是一种可行的证明技巧？

  这个问题实际上有些莫名其妙，归纳的概念多多少少是作为公理存在的，在解释归纳的直觉之前，我们可以先一种比较常规的办法来证明归纳法

令 $\N$ 是自然数集，$P(n)$ 是一个 $\N$ 上的归纳属性，由归纳属性的定义，有 $P(0)$ 成立，令 $S = \lbrace n\in \N\ | \ \neg P(n)\rbrace$，则 $S\subseteq \N$，由 well-ordering principle，存在 $s=\min(S)$ 且 $s\neq 0$，则 $s-1\notin S$，这意味着 $P(s-1)$ 成立，则由归纳属性的定义，$P(s)$ 同样成立，与 $S$ 的定义矛盾，因此 $P(n)$ 对所有 $n\in\N$ 都成立。

这个证明很简单，但是如果对归纳法有一些了解的话，就会发现我们也能用归纳法来证明 well-ordering principle，这就让这么一个证明多多少少变得有些像是循环论证。事实上，与其被理解成一种需要和自然数有关的定理，归纳法更适合被当成一个对自然数的 reformulation，描述归纳法的过程正是描述自然数集的过程。或者可以说，实际上归纳法就是对自然数的定义的一部分。首先，根据定义，我们知道自然数满足 $\N= 0\ |\ S(\N)$¹，这就允许我们把归纳论证想象成一个“尝试构造自然数集的过程”，令 $P(n)$ 是一个归纳命题，归纳论证背后的直觉如下：

令 $S=\lbrace n\in \N \ |\ P(n)\rbrace $ 是一个被 $P(n)$ 所确定的集合，由于 $P(n)$ 是一个归纳属性，显然有 $1\in S$，同理，有 $2\in S$，且对于任意 $n\in S$，都有 $n+1\in S$，这意味着 $S$ 符合自然数的定义，即 $S=\N$

从上面的论证可以看出，归纳论证的过程实际上是说 $P(n)$ 的外延是 $\N$，因此 $P(n)$ 对所有 $\N$ 成立，这意味着某种程度上归纳论证可以被看做是对自然数定义的另外一种描述。
  接下来，让我们从集合的角度来审视一下归纳，令 $F: \mathcal{P}(U) \rightarrow \mathcal{P}(U)$ 是一个函数，如果对于 $A, B\in \mathcal{P}(U)$ 且 $A\subseteq B$，有 $F(A)\subseteq F(B)$，则称 $F$ 为单调的，令 $X\in \mathcal{P}(U)$，如果 $F(X)\subseteq X$，则 $X$ 是 $F$-closed 的；如果 $X\subseteq F(X)$，则 $X$ 是 $F$-consistent 的，如果 $F(X)=X$，则说 $X$ 是 $F$ 的一个 不动点。
  这样的单调函数 $F$ 可以被当作是一个“推理函数”，它的参数是一组逻辑语句，而 $F$ 负责“看看由这一组逻辑语句能推出什么新的语句”，$F$-closed 集合意味着这些定理是 self-contained 的，无法再推导出什么新的定理，而 $F$-consistent 意味着这个集合中的所有定理都是由同样在这个集合中的定理推出来的：假设 $A, B\vdash C$, 则 $F(\lbrace A, B \rbrace)=\lbrace A, B, C\rbrace$，也即证明新定理 $C$ 的所有定理都已经在 $\lbrace A, B\rbrace$ 中。从这个角度来理解，为什么 $F$ 是单调的也就很显然了，因为推理关系 $\vdash$ 可以被当作一个序关系，直觉上，可以把 $F$ 理解成一个“从较小的元素产生较大的元素的生成函数”，例如在上面的例子中，如果将 $\vdash$ 比做一个序关系，那么 $A, B$ 显然是 $C$ 的 predecessor，而 $F$ 则从 $\lbrace A, B\rbrace$ 生成了他们的 successor $C$，此时如果 $F$ 不是单调的，就会出现 derivation tree 中的 premise 被 conclusion 所推导出来的荒谬情况。

例如，如果令 $F(\lbrace A, B\rbrace)=\lbrace A, B, C\rbrace$，$F(\lbrace A, B, C\rbrace)=\lbrace A, B\rbrace$，则 $F$ 不是单调的，而从我们把 $F$ 解释为 $\vdash$ 的语义来看，这显然是荒谬的。

在之后我们将 $F$ 解释为其他函数时，无论是解释为自然数的 $succ$ 函数、逻辑的 implication，还是解释为序关系上的小于等于，语义上也处于同一原因同样满足这个单调性的特点，即从作为 predecessor 的元素，生成作为 successor 的元素。
  让我们首先看一下这样的 $F$ 是如何和归纳扯上关系的

Knaster-Tarski 定理: 令 $U$ 是一个集合，$F:\mathcal{P}(U)\rightarrow\mathcal{P}(U)$ 是一个 $U$ 上的单调函数，则 $F$ 的最小不动点 $\mu F$ 是所有 $F$-closed 集合的交集，而 $F$ 的最大不动点 $\nu F$ 是所有 $F$-consistent 集合的并集。

因此，可以很直观的推导出：

1. （Principle of Induction）对于所有的 $F$-closed 集合 $X$，$\mu F\subseteq X$
2. （Principle of Coinduction）对于所有的 $F$-consistent 集合 $X$，$X\subseteq \nu F$

先放开第二条不管，只看第一条，第一条告诉我们，如果要证明 $\mu F\subseteq X$，只需要证明 $X$ 是一个 $F$-closed 的集合，这意味着什么呢？注意到，我们将 $F$ 当做一个生成函数来对待（你可以把 $F$ 想象成一个对应了 inference rules 的函数），又因为 $\mu F$ 本身是 $F$-closed 的，这意味着 $\mu F$ 是一个 inductive set（任何 $F$-closed 集合都可以通过先选择其中的一部分元素作为 generator，然后递归的调用 $F$ 得到）。现在，结合上面所提到的，归纳的证明过程本质上是证明某个归纳命题 $P$ 的外延是 $\N$²，而 $\N$ 就是一个 inductively defined set，因此，我们可以令 $\mu F=\N$ 并且使用如下设置：

令 $U=\N$，$S: \mathcal{P}(\N)\rightarrow \mathcal{P}(\N)$ 是自然数的 $succ$ 函数，也即 $S(X)=\lbrace 0\rbrace\cup \lbrace x+1\ |\ x\in X\rbrace $，则 $\mu S$ 显然是 $\N$，令 $P$ 是 $\N$ 上任意归纳属性的外延（或者说 $P$ 是 $\N$ 上的任意 inductive set），则如果 $S(P)\subseteq P$，也即 $P$ 是 $S$-closed 的，则 $\N\subseteq P$，又因为 $P$ 是 $\N$ 上的 inductive set，因此 $P$ 至多等于 $\N$，即如果 $P$ 是 $S$-closed 的，则 $P=\N$。

回顾一下之前说过的“归纳法背后的直觉”，里面提到了归纳法的本质基本上是定义了一个 $\N$，或者说证明某个归纳命题的外延是 $\N$，而这就正是我们上面所描述的，通过引用 Principle of Induction，要证明某个属性 $P$ 对所有 $n\in \N$ 都成立，我们只需要证明这个属性 $P$ 的外延是 $S$-closed 的，也即 $S(P)\subseteq P$，这意味换句话说，只需要证明

对于所有的 $x\in\ N$，如果 $x\in P$，那么 $S(x)\in P$。

如果将 $S(x)$ 的定义展开，这蕴含了

$0\in P$，且对于对于所有的 $x\in\N$，如果 $x\in P$，那么 $x+1\in P$

而这恰好是对归纳法的描述。

  在本文中，我们将 Induction 作为一种证明技巧来对待，并且通过取对偶提出了 Coinduction 这一种证明技巧，同时还对这两种技巧进行了数学上的 formulation 和合适的 generalization。，在本文的下一个章节中，我们会从类型的视角了解 Inductive Type 和 Coinductive Type，以及他们之间、尤其是在 finiteness 上的异同。

本文中只包含了最核心的功能代码，一些工具函数等则不会列出，如果想要了解完整的实现，请前往 GitHub

  鉴于本系列的目的是实现一个内存管理器，因此在内存分配器这方面，我并不打算下太多功夫，但是在此刻不放让我们抛出一个问题来抛砖引玉：内存管理器和内存分配器究竟又有什么区别呢？
  这个问题的答案倒也没那么复杂，内存分配器可以视作内存管理器的一部分，在一个编程语言的运行时中，一个内存管理器应当能够分配对象，销毁对象，合理的利用和管理内存资源，保证利用效率的最大化。许多人会认为垃圾回收器是内存管理器的一部分，然而在很多语言的实现中，这两者实际上是同义词：垃圾回收器不仅要负责回收不用的对象，还要负责压缩内存空间，以及分配新内存。
  如果我们要分配一个对象，第一部自然是分配和这个对象的大小相同的一块内存，那么内存分配器该如何实现呢？现在的大部分 OS 上，都有现成的暴露出来的内存分配和回收函数（例如 C 的 malloc 和 free 等函数在 Unix 和 Windows 上实际会指向不同的平台实现），我们所要做的只是调用这些函数而已，不过对于一个完整的内存管理器来说，我们还需要考虑另外一点：内存碎片
  想必点进本文的读者应该都知道，应用的内存区域中有一块空间叫做堆空间，专门用来给程序运行时的较大内存分配使用，可是，堆内存的空间是有限的，其中的对象不会自己移动，如果我们随便的在堆中分配并且释放对象，整个堆就会像被扎满孔的海绵一样，虽然总体来看剩的空间还很多，但是分开来看每一段都是一块很小的内存碎片，难以容下需要一大块连续内存的对象分配。
  这个问题——尽管相当有年头，却也是一个非常棘手的问题，一些内存分配器会采取一些聪明的策略，比如用类似线段树这样的结构去维护被分配的内存区间，一旦其中有两块相邻的内存碎片都被回收，就马上把他们两个合成一块大的碎片。这样的策略相当之有效，然而其问题依然在于无法做到 100% 的利用内存空间，总有些内存碎片碎片不会那么恰巧的被一同回收，使用这样内存分配器的语言于是会相当的考验其实现者和使用该语言的人的技术。
  幸运的是，我们不需要考虑这个问题，我们所要实现的内存管理器，正是一个垃圾回收器，确切的说，是一个 标记-压缩垃圾回收器，这意味着每当一批对象被回收之后，我们的内存管理器就会通过移动剩余的对象来压缩空间（有点像是把一管松散的羽毛球全部捅到最里面），从而彻底避免内存碎片的问题，不仅如此，因为不用思考内存碎片的问题，我们的内存分配器可以采用一种叫做 Bumping Pointer 相当简单而且速度异常快的内存分配策略，简单来说，如果把内存想象成一个线性的字节数组，那么我们的内存分配器会有一个指针指向尚未分配的内存起始，当我们需要特定大小的内存的时候，只需要将这个指针向后移动对应长度的距离，接着返回指向这一段内存的一个指针就好了。无须任何复杂的数据结构，这样的一个内存分配器的分配速度永远是常数级别的。
  说了这么多，也终于到了该写一点代码的时候了，首先，我们的内存分配器应当在在最开始向操作系统申请一大块内存，叫做已提交的内存，在程序的运行过程中，像这样“从操作系统申请一大块内存”的操作可能会发生多次，因为上一次申请的内存可能不够用，我们把每次申请到的这一大块内存称为一个 HeapBlock，这样，我们的内存分配器就至少需要一个列表，来维护所有分配的 HeapBlock，而 HeapBlock 的实现如下：

#[derive(PartialEq, Eq, Hash, Copy, Clone)]
pub struct HeapBlock {
    pub start: *mut u8,
    pub unallocated_start: *mut u8,
    pub size: usize,
}

impl HeapBlock {
    pub fn contains(&self, ptr: *mut u8) -> bool {
        let start = self.start as usize;
        let end = start + self.size;
        let ptr = ptr as usize;
        ptr >= start && ptr < end
    }

    pub fn relative_offset<T>(&self, ptr: *const T) -> usize {
        let start = self.start as usize;
        let ptr = ptr as usize;
        ptr - start
    }

    pub fn absolute_offset<T>(&self, offset: usize) -> *mut T {
        unsafe { self.start.add(offset) as *mut T }
    }

    pub fn block_end(&self) -> *mut u8 {
        unsafe { self.start.add(self.size) }
    }

    pub fn allocated_size(&self) -> usize {
        unsafe { self.unallocated_start.sub_ptr(self.start) }
    }
}

其所包含的都是一些相当基本的函数：unallocated_start 是我们指向未分配内存块的指针，start 是当前 HeapBlock 的起始位置的指针，而 size 是这块内存块的长度。其余的函数应该都是不言自明的，我们有：

• contains 检查某个指针是否位于当前 HeapBlock 内
• relative_offset 返回某个指针相对于当前 HeapBlock 起始的距离
• absolute_offset 返回距离当前 HeapBlock 起始位置距离为 offset 的指针
• block_end 返回当前 HeapBlock 的末尾
• allocated_size 返回当前 HeapBlock 中已被分配的内存的大小

接下来，我们就要实现基于此的 HeapAllocator，也就是我们的内存分配器了，其描述如下：

pub struct HeapAllocator {
    pub size: usize,
    pub committed_regions: LinkedHashMap<Layout, HeapBlock>,
    pub expand_callback: Box<dyn FnMut(HeapBlock)>
}

其中 committed_regions 即为程序所持有的所有内存块，Layout 是 Rust 中的一个类型，描述了这个内存块的布局，在此不用过多了解，expand_callback 是在分配新的内存块，也就是向 committed_regions 中插入新的项时被调用的回调。而 size 则是目前分配器已经分配的内存的总大小

  在程序开始执行之前，我们还没有向操作系统申请任何内存，因此，向操作系统申请一块新的内存，自然是我们要做的第一件事，这个函数被命名为 expand，这个函数的签名如下：

unsafe fn expand(&mut self, desired_size: usize, align: usize) -> Result<(), AllocatorError>

desired_size 告诉操作系统我们要申请的内存块有多大，而 align 则表明了这块内存的对齐（也就是说，这块内存的大小应该是 align的整数倍），这是因为现代 CPU 对于地址对齐之后的读写操作效率更高。在这个函数中，我们首先要判断真正要申请的内存块究竟有多大：

let mut new_layout_size = if self.size == 0 { INITIAL_SIZE } else { self.size * EXPAND_FACTOR };
if new_layout_size < desired_size {
    new_layout_size = (desired_size + ((!desired_size + 1) & (align - 1))) * EXPAND_FACTOR;
}

如果 desired_size 是0，那么我们就会用一个默认大小作为分配大小，如果不是0，我们首先会尝试将分配大小设定为当前已分配总大小的 EXPAND_FACTOR 倍，其中这个倍率大小可以自由决定（如果我们不考虑一些硬件层面的优化的话），这样是为了使每次扩展堆时，堆大小的增长符合一个大致的规律，不至于太大浪费内存，也不至于太小让分配的内存总是不够用（我相信一定有一些启发性的算法来动态决定这个 EXPAND_FACTOR 的大小，可惜这样的内容不在本文的范围之内）。如果这样尝试之后，新内存块的大小依然不足以容纳 desired_size，那么我们会干脆把其大小设置为 desired_size 的 EXPAND_FACTOR 倍，这里用了一点小小的位运算，这个位运算的作用是把新内存块的大小向上取至 align 的整数倍，从而满足对齐的要求。

  在完成新内存块大小的分配后，要做的事情就是分配内存了，这里要利用到 Rust 的内存分配API，准确来说，是 std::alloc 下的类型，Rust 的内存分配要求传入一个用于描述要分配的类型的对象，也就是 Layout 对象，在这里，我们要分配的应该是一个指定大小的字节数组（也就是内存的本质），因此我们会首先创建这样的一个 Layout，接着修改目前已分配的总内存大小，最后，我们调用 std::alloc::alloc_zeroed(new_layout) 来向操作系统申请一块新内存，这个函数会返回一个指向我们申请的内存的首地址：

let new_layout = match Layout::array::<u8>(new_layout_size) {
    Ok(l) => l,
    Err(_) => return Err(AllocatorError::FailedToCreateLayout)
};
self.size += new_layout.size();
let ptr = alloc::alloc_zeroed(new_layout);

  最终，在申请完成之后，我们要为这片内存创建一个对应的 HeapBlock 对象，用来在我们之后的代码中作为这一块内存的抽象和描述符（Rust 自带的 Layout 显然是不够用的）

let region = HeapBlock {
    start: ptr,
    unallocated_start: ptr,
    size: new_layout.size()
};
self.committed_regions.insert(new_layout, region);
(self.expand_callback)(region);

（注意此处调用了 self.expand_callback，也就是我们说的在堆扩容时会被调用的函数）

  于是最终，我们的堆扩容函数就变成了这个样子：

unsafe fn expand(&mut self, desired_size: usize, align: usize) -> Result<(), AllocatorError> {
    // 计算要扩容的真实大小
    let mut new_layout_size = if self.size == 0 { INITIAL_SIZE } else { self.size * EXPAND_FACTOR };
    if new_layout_size < desired_size {
        new_layout_size = (desired_size + ((!desired_size + 1) & (align - 1))) * EXPAND_FACTOR;
    }
    // 向操作系统申请内存
    let new_layout = match Layout::array::<u8>(new_layout_size) {
        Ok(l) => l,
        Err(_) => return Err(AllocatorError::FailedToCreateLayout)
    };
    self.size += new_layout.size();
    let ptr = alloc::alloc_zeroed(new_layout);
    // 创建这一块已分配内存的描述符，也即 HeapBlock
    let region = HeapBlock {
        start: ptr,
        unallocated_start: ptr,
        size: new_layout.size()
    };
    self.committed_regions.insert(new_layout, region);
    (self.expand_callback)(region);
    Ok(())
}

  在实现了 expand 函数之后，就如同上面所说的，用于分配的 alloc 函数就要简单的多了，它的函数签名如下：

unsafe fn alloc(&mut self, size: usize, align: usize) -> Result<*mut u8, AllocatorError>

其中 size 的含义不言自明，而 align 这次则和 expand 中的有些不同，在 expand 中，内存分配是操作系统负责的，我们只需要保证分配的内存大小是对齐的，而不需要思考其地址是否对齐，但是在 alloc 函数中，我们需要自己分配内存，因此在此处我们要手动将分配内存的起始位置对齐为 align 的整数倍，如果不是整数倍，我们就需要在前面 垫 一下，跳过几个地址，来保证分配的地址始终是整数倍的，这些被跳过的地址被称为 padding。在 alloc 函数中，我们首先应当找到所有已分配内存块中第一个能容纳下我们要分配的大小的那个：

// 找到第一块有足够空间的内存块
let first: Option<&Layout, &mut HeapBlock> = self.committed_regions.iter_mut().find(|entry| entry.1.allocated_size() + size <= entry.1.size);

接下来，如果其返回的对应的内存块，说明我们还有足够的空间直接在里面进行分配，如果不是，则说明我们的堆空间耗尽，需要向操作系统申请新的内存，也即扩容，之后再重新尝试分配：

match first {
    Some((_, tracker)) => { // tracker: &mut HeapBlock
        // 注意这里是让分配的起始地址对齐
        let padding = (!(tracker.unallocated_start as usize) + 1) & (align - 1);
        // 向 unallocated_start 填充 padding
        tracker.unallocated_start = tracker.unallocated_start.byte_add(padding);
        let ptr = tracker.unallocated_start;
        // 将未分配内存起始的指针向后移动对应长度，代表我们“分配”了这一块内存
        tracker.unallocated_start = tracker.unallocated_start.byte_add(size);
        Ok(ptr)
    },
    None => {
        // 如果找不到能容纳所需大小的内存块，则对堆进行扩容
        self.expand(size, align)?;
        // 之后再尝试分配
        self.alloc(size, align).map(identity_once)
    }
}

因此在最后，我们的 alloc 函数就变成了这样子：

pub unsafe fn alloc(&mut self, size: usize, align: usize) -> Result<*mut u8, AllocatorError> {
    if !self.available {
        return Err(AllocatorError::AllocatorClosed);
    }
    let first = self.committed_regions.iter_mut().find(|entry| entry.1.allocated_size() + size <= entry.1.size);
    match first {
        Some((_, tracker)) => {
            let padding = (!(tracker.unallocated_start as usize) + 1) & (align - 1);
            tracker.unallocated_start = tracker.unallocated_start.byte_add(padding);
            let ptr = tracker.unallocated_start;
            tracker.unallocated_start = tracker.unallocated_start.byte_add(size);
            Ok(ptr)
        },
        None => {
            self.expand(size, align)?;
            self.alloc(size, align).map(identity_once)
        }
    }
}

  现在可以说我们的内存分配器已经处于“整装待发”的状态了，要说还缺点什么，那就是释放内存的能力了，不过这倒也很好实现

pub unsafe fn free(&mut self) {
    for (layout, tracker) in self.committed_regions.iter() {
        alloc::dealloc(tracker.start, *layout);
    }
    self.available = false;
}

不过，想必你已经注意到，这个函数会一次性释放堆中的所有内存，它的作用是在程序执行完毕时释放程序占用的内存空间，至于针对单个对象的 free 函数——我们都有垃圾回收器了，为什么还需要这种东西呢？

  既然内存分配器的部分已经讲完了，本文的下一节就将会讲述更抽象的概念：我们该如何分配一个对象呢？与内存分配器的简单相比，对象分配器则要复杂得多，在下一节中，我们将会讨论对象的内存布局，对象头与对象数据，向内存中写入对象，以及从内存中的某个地址读取对象，其所使用到的内存分配器就将会是我们本节所实现的。本文实现的详细代码位于 src/allocator/heap_allocator.rs 中，如果对本文的实现有疑问，或者想要完整的了解代码，包括一些工具函数，可以前往该项目查看。

[google-translator]

  Il y a beaucoup de livres sur la théorie axiomatique des ensembles, ces livres vous introduiront les axiomes, principalement les axiomes du système de ZFC, mais il y en a moins qui vous expliquer pourquoi on choisit ces axiomes, au lieu des autres, dans cette article, je vous introduirai l'expérience mentale derrière les théories axiomatiques des ensembles, et comment peut-on dériver ces axiomes.

La hiérarchie cumulative-itérative.

  Le désavantage majeur de la théorie ramifiée des types de Russell, c'est que cette théorie n'est pas vraiment pratique à appliquer: il y a eu des théorems qui utilisent des définitions imprédicatives, mais en même temps n'exposent pas de paradoxe, ces définitions imprédicatives ne seraient pas aussi mals, mais notre théorie ramifiée des types les rejete tous.

  Qu'est-ce que la bonne imprédicativité et qu'est-ce que la mauvaise imprédicativté? Comment peut-on les distinguer? Pour y répondre, rappelons la définition d'imprédicativité:

Une définition s'appelle imprédicative, si la quantification de cette définition invoque certaines formes de totalité d'un genre quelconque d'objets, et y définit un nouvel objet.

  Mais, il est objecté qu'il y ait des définitions imprédicatives qui ne déclenchent pas de paradoxe. Observons la définition: "le personne le plus grand parmi tous les humains", "l'ordinateur le plus rapide parmi ce groupe d'ordinateurs", ces définitions sont imprédicatives, et ils se partagent une propriété spéciale: malgré qu'ils soient imprédicatives, ils peut se spécifier, ou dit, se construire, sans aucun référence à l'imprédicativité, on peut simplement pointer ce personne ou cet ordinateur. Il est donc dit, par Frank Ramsey, qu'une définition imprédicative soit male si et seulement si l'on ne peut pas le spécifier d'une autre manière prédicative. ¹

  Il est donc proposé, une autre vue d'ensembles, on considère les ensembles comme des objets mathématiques construits, au lieu d'une collection de certaines objets mathématiques satisfaisant des propriétés arbitraires (on l'abrège souvents comme Compréhension Naïve, où l'ensemble lui-même vient de nulle part, on ne l'a jamais construit, on l'a décrit simplement).

  Le processus de ce genre de constructions ressemble à celui de la théorie ramifiée des types: il y a des différents genres d'ensembles, ramifiés en différents niveaux, cependant, à la différence de la théorie des types, cette ramification agit au processus de la construction, au lieu des ensembles eux-mêmes; donc tous les ensembles sont. c'est-à-dire, encore ensembles, il n'y a pas d'univers différents $Set_1$, $Set_2$, ..., $Set_n$ qui les séparent, et par suite évite les désavantages de la théorie des types.

Les axiomes, ils viennent d'une expérience mentale

  Le processus on a introduit ci-dessus s'appelle la hiérarchie cumulative-itérative, il construit tous les ensembles possibles étape à étape, c'est en fait une expérience mentale: tout ensemble a une propriété supplémentaire: son étape auquel il est formé, les étapes ont des ordres, chacun de ces étapes a certaines étapes avant lui, et les ensembles à chaque étape se construit d'ensembles dont l'étape est avant eux.

  L'itération est un processus fini mais peut être exécuté ad infinitum, alors il devrait y avoir un premier étape tel qu'il n'y ait pas d'étape avant lui et donc pas d'ensembles peut s'utliser pour y construire les ensembles, alors, on peut seulement y former un seul ensemble: l'ensemble vide $\empty$, au ètape suivant, il y a évidemment un ensemble $\empty$, et un autre ensemble $\lbrace \empty\rbrace$, alors à cet étape on a deux ensembles $\empty$ et $\lbrace \empty\rbrace$, il se trouvera, sans aucun difficulté, qu'au troisième étape on a $\empty$, $\lbrace \empty\rbrace$, $\lbrace \empty,\lbrace\empty\rbrace\rbrace$, ce processus s'étend ad infinitum et on aura $\lbrace\empty,\lbrace\empty\rbrace, \lbrace \empty,\lbrace\empty\rbrace\rbrace\rbrace$, $\lbrace\empty,\lbrace\empty\rbrace, \lbrace \empty,\lbrace\empty\rbrace\rbrace, \lbrace\empty,\lbrace\empty\rbrace, \lbrace \empty,\lbrace\empty\rbrace\rbrace\rbrace\rbrace$, etc. Et il n'y a pas d'ensemble que ces ensembles formés.

  Je suppose que vous seyez quelqu'un qui avez certaines compréhensions sur la théorie axiomatique des ensembles, si c'est le cas, vous trouveriez peut-être que ça nous dise qu'il y a une infinité d'ensembles, en effect et de plus, tous les axiomes de la théorie peut être dérivés (ou dit, expliqués) à partir de cette expérience mentale. Par exemple, voyons encore une fois l'axiome de compréhension, c'est indéniablement le concept le plus important dans la théorie des ensembles, il nous permet de construire des ensembles raisonnables. Soit $A$ un ensemble, par notre hiérarchie, $A$ est formé à un certain étape $S$, alors il doit y avoir des étapes avant $S$, et tous les éléments de $A$ sont formés à ces étapes, maintenant soit $\varphi$ une fonction propositionnelle, on peut choisir les éléments satisfaisant $\varphi$ et apparaissant à $A$, donc on aura un nouvel ensemble $\lbrace x\in A | \varphi(x)\rbrace$. Cet ensemble est bien défini à l'égard de la hiérarchie: puisque tous ces ensembles apparaissent à $A$, leur existence est justifiée (cf. l'explication ci-dessus), et puisque ils sont des ensemble avant $S$, alors au étape $S$ on peut construire un ensemble les contenant exactement, i.e., $\lbrace x\in A | \varphi(x)\rbrace$. En écrivant cette observation en un langage logique, on a schéma d'axiomes de séparation, i.e., on a séparé un ensemble à partir de $A$, il dit: chaqun des prédicates $\varphi(x)$ correspond à un ensemble:

$$
\forall A. \exists S.\forall x. [x\in S\iff (\varphi(x)\land x\in A) ]
$$

L'ensemble $S$ est exactement notre nouvel ensemble.

  La théorie axiomatique des ensembles est créée pour éviter le paradoxe de Russell, alors pour justifier notre expérience mentale, on a besoin de voir qu'il est capable d'éliminer le paradoxe. Rappelons la formulation du paradoxe de Russell:

$$
R=\lbrace x\in A | x\notin x\rbrace
$$

Cet ensemble n'est pas paradoxal dans notre cadre: tous les éléments de $R$, ce qui sont des éléments de $A$, ce qui à son tour sont des ensembles qui sont formés avant l'étape de $S$, $R$ ne peut pas donc contenir lui-même, car un ensemble ne peut pas contenir un autre ensemble ayant le même étape.

Regarding the education of the computer science, I once read an answer on a Q&A site about "how to learn compiler construction". Most people answer with the typical recommendation: Compilers: Principles, Techniques & Tools, which is also the book that inspired me back to those days, however, in that answer there was a different voice: an anwser demanded the poster to read SICP (i.e. Structural interpretation of Computer Programs), and says this book is exactly for the beginner at such areas including compiler construction or more general computer science. I have to confess that by that time I was angered, and assured that by doing such things will only lead the beginners astray, because it is too abstract and meanwhile it's hard to understand intuitively, such an overcomplicated concept intoduction will twist the mind of those beginners.

And, perhaps, you may ask, as such a person that is passionate on the PLT and related mathematics, have you changed your mind? Do you now agree that Racket/LISP the best language for introducing newbies to the field of computer science?

No, my friend, I respectifully refuse. In fact, even now I know little LISP/Racket.

That must means you object your friend's opinion!

No, my friend, I respectifully refuse. In fact, I must be one of the firmest supporter. But I have to clarify some unfortunate facts.

First, introducing SICP to a first-year undergraduate student is hard, it's kinda like introducing C++ to a person that doesn't know no shit about programming before, he will learn, honestly, he will learn, but only its mere surface, the real iceberg still lies under. The real things the author wants to convey is impossible for most beginnners, I kindly invite the reader to pause and reflect, especially when you are a person that have a considerable knowledge for the theory of computation, aren't there so many new things you learned the second time you read the book? Without some mathematical preliminaries, it is hard to learn such books effectively. What do you think of the Kleene Closure at the first glance, can you treat it as a free monoid and connect it to other part of the mathematics and by doing so, connect (or model) the automata theory with classical parts like algebra? Or some more advanced concepts like categories? What do you think about types then? Does "Types are higher groupoids" mean anything to you, do you have had a even slightest idea that connects the topology and logic? despite of the fact that the connection between these two fields have been existed for long?

Second, you may ask, why don't we just learn math first, well, techniquely possible but pratically, it's rather impratical: (, first, the learning process is not sequatial but parallel, meaning in most times this two courses with be taught à la fois, moreover, that kind of math is also very abstract, the theory of computation is part of mathematical logic which is built upon a rigorous yet abstract system of string manipulation (the 101 course may not introduce those rigorous logical notations and concepts, but still the level of abstraction is a bit too high for first-year undergrads), which is quite the opposite of almost all the mathematics we learned in our senior school (no one have ever thought we really need to deal with the equal sign in $1+1=2$

In a system with a built-in sense of computation? perhaps? does $1+1=2$ equals intentionally which means the left side computes to the right side and they are basically the same thing with different syntax, or equals extensionally, which means for all functions (including propositional functions, that is to say) yields the same results, do we have anything to witness such equalities so that they are nolonger metatheoretical results? which means they equals propositionally, oh but wait, isn't "equality" such a simple concept that we have learned back to the very years when we are still in our preschool? Why do we have to introduce such mysterious terms? What is the relation between propositional equality and extensional equality? The former witnesses the latter, perhaps? And what about the definitional equality and extensional equality? The former clearly implies the latter because former equality states fundamentally two same things, that they are interpreted to the same semantic interpretation, but what about the reverse direction?

or how can we generalize the action of replacing a character with another character to the concept of a computer: that is, capable of doing arithmetic calculations, let alone the difficulty of things like theorem proving!). As a first year undergrad, jumping from evaluating the trigonometric functions to the axioms and theorems is somewhat a big leap, I'm not saying that the latter is really harder than the former, but the way of thinking is way too far.

In countless time of similar discussions, at this point, I were about to make a little digression on the importance of self-study, but this is certainly already mentioned in my friend's post, so I will talk about something different: The education is kinda tricky, think of it, why is our society be filled with the so called "software engineers" (no offense to the real software engineers, here I refer to those knows nothing except java, asking them anything about java's darkest secrets and they shall answer you with a marvelous fluency, but their real enginneering capability is so terrible and what they have memorized, they don't know the reason.). Because our education and the job require them to do so! I can't blame such persons, because I do feel like that if they were properly educated, they should have accepted the beauty and elegancy of the theoretical computer science (Booing: Arrogance!). But I do believe this is the fact, the reason is just that the demands of society do not need the understanding of theoretical foundations, you just need to know how to use it. And that why so many people say that "languages are just tools!", it's not wrong, but the way you view matters (That's why I say "I do not agree with the famous slogan: 'for languages, there is no good and bad, there is only suit or not.'")

Again, in countless times, I cast my contempt on those programmers, engineers, and undergrads, that they are either too silly to learn the even simplest concepts (complaining how hard is the undergraduate-level compiler construction), or they are filled with the terrible ignorance so that they don't see the importances of the theoretical foundations of the things on which they are working, and I used to like to share and make fun on these cases with my friends, I have to admit that, this kind of idea is originated purely from my arrogance and ego, once when I, like all the old days, sharing these news and posts with my friends in the chat, my friend responded me with a quote that he saw on a Q&A website: "I started to consider that, not every IT employees or students are so eager to acquire these knowledges just like I do, these persons, their intentions may vary, some of them seeks knowledge, and some of them just want to make a living, their interests stay elsewhere, and I cannot judge them simply from my own perspective." I was really persuated, because I am exactly the kind of person to whom the quote refers. Here I'd like to throw a question to the readers: What should we criticise? These persons? The outdated technologies, methodologies, and educations? I think the answer would be none, this is a pathetic fact that we have to accept: criticizing anyone of them separately is rather inappropriate, yet criticizing them all together seems too cynical. Yes, it is really, really pathetic that most of the IT workers don't care about the essence of this vast area, but only for us —— this is not ego, this is specialization, just like a lot programmers can't understand why those illustrators protest against AI generated contents, I believe those illustrators share the same attitude toward these programmers as how we think of the "current industry". So here and now, although with the same belief, I derived something different compared to that of my friend's: It is a pathetic story, and we have to tolerate it, and no one should be blamed. (除了他妈的现在还在用VC 6.0和VB的脑残高中微机课和大学课程，遇见这种上面说的全部作废)