Comment pouvons-nous surmonter les temps de compilation et les délais d'exécution lors de la programmation dans un langage à typage dépendant?

Question

Je me suis dit qu'en dépendant du type de système, les "types" et de "valeurs" est mixte, et nous pouvons traiter tous les deux "conditions" à la place.

Mais il y a quelque chose que je ne comprends pas: dans un fortement typé langage de programmation sans Type de charge (comme Haskell), Types est décidé (inférer ou vérifié) au moment de la compilation, mais les valeurs est décidé (calculée ou d'inscription) à l' exécution.

Je pense qu'il doit y avoir un écart entre ces deux étapes. Il suffit de penser que si une valeur est de manière interactive lire à partir de STDIN, comment pouvons-nous la référence de cette valeur dans un type qui doit être décidé AOT?

par exemple, Il existe un nombre naturel n et une liste de naturel nombre xs (qui contient n éléments), que j'ai besoin de lire à partir de STDIN, comment puis-je les mettre dans une structure de données Vect n Nat?

Answer 1

Supposons que nous sommes à l'entrée n :: Int lors de l'exécution formulaire de STDIN. Nous avons ensuite lu n des chaînes, et de les stocker en vn :: Vect n String (semblant pour l'instant, ce qui peut être fait). De même, on peut lire, m :: Int et vm :: Vect m String. Enfin, nous concaténer les deux vecteurs: vn ++ vm (en simplifiant un peu ici). Cela peut être vérifié, et de type Vect (n+m) String.

Maintenant il est vrai que le vérificateur de types s'exécute au moment de la compilation, avant que les valeurs n,m sont connus, et aussi avant d' vn,vm sont connus. Mais ce n'est pas grave: on peut toujours raison symboliquement sur les inconnues n,m , et dire que d' vn ++ vm a ce type, impliquant n+m, même si nous ne savons pas encore quel n+m est en réalité.

Il n'est pas si différent que ça de faire des mathématiques, où l'on manipule des expressions symboliques impliquant des variables inconnues, selon certaines règles, même si nous ne connaissons pas les valeurs des variables. Nous n'avons pas besoin de savoir quel est le nombre n de voir qu' n+n = 2*n.

De même, le type checker permet de vérification de type

-- pseudocode
readNStrings :: (n :: Int) -> IO (Vect n String)
readNStrings O     = return Vect.empty
readNStrings (S p) = do
   s <- getLine
   vp <- readNStrings p
   return (Vect.cons s vp)

(Eh bien, en fait, certains de plus d'aide de la programmeur pourrait être nécessaire pour typecheck, puisque cela implique dépendante de la correspondance et de la récursivité. Mais je vais négligence à ce sujet).

Surtout, le type de vérificateur peut vérifier que, sans le savoir ce qu' n est.

Notez que la même question déjà soulevée par des fonctions polymorphes.

fst :: forall a b. (a, b) -> a
fst (x, y) = x

test1 = fst @ Int @ Float (2, 3.5)
test2 = fst @ String @ Bool ("hi!", True)
...

On peut se demander "comment l'typechecker vérifiez fst sans savoir à quels types a et b sera au moment de l'exécution?". Encore une fois, par un raisonnement symbolique.

Avec des arguments de type c'est sans doute plus évident puisque nous avons l'habitude d'exécuter les programmes après l'effacement, à la différence de la valeur des paramètres tels que notre - n :: Int - dessus, qui ne peuvent pas être effacées. Encore, il ya une certaine similitude entre universellement quantifier plus de types ou plus Int.

Answer 2

Il me semble qu'il y a deux questions ici:

1. Étant donné que certaines valeurs sont inconnues lors de la compilation (par exemple, les valeurs lues depuis l'entrée standard STDIN), comment peut-on les utiliser dans les types? (Notez que chi a déjà donné une excellente réponse à cela.)

2. Certaines opérations (par exemple, getLine) n'a absolument aucun sens au moment de la compilation; comment pourrions-nous nous parler d'eux dans les types?

La réponse à (1), chi a dit, est symbolique ou de raisonnement abstrait. Vous pouvez le lire dans un certain nombre n, et ensuite une procédure qui s'appuie Vect n Nat par la lecture à partir de la ligne de commande n temps de, faire usage de l'arithmétique des propriétés telles que le fait qu' 1+(n-1) = n pour les nombres naturels non nuls.

La réponse à (2) est un peu plus subtil. Naïvement, vous voudrez peut-être dire "cette fonction renvoie un vecteur de longueur noù n est lu à partir de la ligne de commande". Il existe deux types de vous pouvez essayer de donner à ce (toutes mes excuses si je suis la notation Haskell mal)

unsafePerformIO (do n <- getLine; return (IO (Vect (read n :: Int) Nat)))

ou (en pseudo-Coq notation, puisque je ne suis pas sûr de ce que Haskell notation pour existentielle types)

IO (exists n, Vect n Nat)

Ces deux types peuvent à la fois être donné du sens, et dire des choses différentes. Le premier type, à moi, dit: "au moment de la compilation, lisez n à partir de la ligne de commande, et le retour d'une fonction qui, au moment de l'exécution, donne un vecteur de longueur n en effectuant IO". Le deuxième type dit "à l'exécution, d'effectuer IO pour obtenir un nombre naturel n et un vecteur de longueur n".

La façon dont je tiens regarde c'est que tous les effets secondaires (sauf, peut-être, non-résiliation) sont monade transformateurs, et il y a une seule monade: le "monde réel" monade. Monade transformateurs de travail aussi bien au niveau du type au niveau de terme; la seule chose qui est spécial, c'est run :: M a -> a qui exécute la monade (ou la pile de la monade transformateurs) dans le "monde réel". Il y a deux points dans le temps au cours de laquelle vous pouvez invoquer run: on est au moment de la compilation, où vous prévaloir d'une quelconque instance de run qui se montre au niveau du type. Un autre est au moment de l'exécution, où vous prévaloir d'une quelconque instance de run ce qui montre jusqu'à la valeur de niveau. Notez que run n'a de sens que si vous spécifiez un ordre d'évaluation; si votre langue ne précise pas si elle est en appel par valeur ou en appel par nom (ou appel par push-valeur ou en appel par nécessité ou appel par quelque chose d'autre), vous pouvez obtenir des incohérences lorsque vous essayez de calculer un type.