2

Je travaille sur un langage de programmation expérimental qui a une inférence de type polymorphique globale.Code qui utilise l'inférence de type

J'ai récemment eu l'algorithme qui fonctionne assez bien pour taper correctement les bits de l'échantillon de code que je lance. Je cherche maintenant quelque chose de plus complexe qui va exercer les cas de bord. Est-ce que quelqu'un peut me pointer à une source de fragments de code vraiment gnarly et horribles que je peux utiliser pour cela? Je suis sûr que le monde de la programmation fonctionnelle a beaucoup. Je suis particulièrement à la recherche d'exemples qui font du mal avec la récursivité des fonctions, car je dois vérifier que l'extension de la fonction se termine correctement, mais tout va bien --- j'ai besoin de construire une suite de tests. Aucune suggestion?

Mon langage est en grande partie impératif, mais tout code de style ML devrait être facile à convertir.

Répondre

3

Ma stratégie générale est en fait de l'approcher de la direction opposée - assurez-vous qu'elle rejette les choses incorrectes!

Cela dit, voici quelques tests "de confirmation" standard que j'utilise habituellement:

Le point fixe désireux combinateur (sans vergogne volé here):

datatype 'a t = T of 'a t -> 'a 

val y = fn f => (fn (T x) => (f (fn a => x (T x) a))) 
       (T (fn (T x) => (f (fn a => x (T x) a)))) 

récursion mutuelle Obvious:

fun f x = g (f x) 
and g x = f (g x) 

Découvrez également ces expressions lettrées profondément imbriquées:

val a = let 
    val b = let 
     val c = let 
     val d = let 
      val e = let 
       val f = let 
        val g = let 
        val h = fn x => x + 1 
        in h end 
       in g end 
      in f end 
     in e end 
     in d end 
    in c end 
in b end 

Fonctions d'ordre supérieur imbriquées en profondeur!

fun f g h i j k l m n = 
    fn x => fn y => fn z => x o g o h o i o j o k o l o m o n o x o y o z 

Je ne sais pas si vous devez avoir la restriction de valeur afin d'incorporer des références mutables. Si oui, voir ce qui se passe:

fun map' f [] = [] 
    | map' f (h::t) = f h :: map' f t 

fun rev' [] = [] 
    | rev' (h::t) = rev' t @ [h] 

val x = map' rev' 

Vous pourriez avoir besoin de mettre en œuvre map et rev de façon standard :)

Puis, avec des références réelles qui traînent (volée here):

val stack = 
let val stk = ref [] in 
    {push = fn x => stk := x :: !stk, 
    pop = fn() => stk := tl (!stk), 
    top = fn() => hd (!stk)} 
end 

Espérons que cela aide d'une manière ou d'une autre. Assurez-vous d'essayer de construire un ensemble de tests de régression que vous pouvez relancer de façon automatique pour vous assurer que toute votre inférence de type se comporte correctement à travers toutes les modifications que vous faites :)

+0

Fantastique --- merci! (Bien que je puisse avoir besoin de remettre mon insigne «tumbleweed».) Mon langage est procédural plutôt que fonctionnel, et utilise une sorte de CPA mutée plutôt que Hindley-Milner, mais je peux adapter la plupart d'entre eux. Si je peux implémenter votre carte 'et rev' en utilisant les fonctions de voiture, de cdr et de contrepoids dans la langue et que ça marche, je serai heureux. Hélas, je n'ai pas de fonctions d'ordre supérieur, mais je vais essayer de trouver un moyen de les faire fonctionner. –

+0

bien, en termes de voiture et cdr, la carte est simplement 'fun map 'f l = si l = [] alors [] cons cons (f (voiture l), carte' f (cdr l))'. rev 'est' fun rev 'l = si l = [] alors [] else ajoute (rev' (cdr l), contre (car l, nil)) ', je suppose. La plupart du temps, je voudrais juste me concentrer sur la génération d'exemples que le vérificateur de type devrait rejeter! – Gian

Questions connexes