Comment définir partiellement les signatures de fonctions en Haskell ?

Question

Point de départ :

fn :: [a] -> Int
fn = (2 *) . length

Disons que nous seulement nous voulons contraindre la valeur de retour, alors nous pourrions écrire :

fn list = (2 * length list) :: Int

Pourquoi ne pas restreindre seulement l'argument ? Facile.

fn list = 2 * length (list :: [Char])

Bien que cela fonctionne, il serait préférable d'avoir les signatures en haut rassemblées et non dispersées dans le corps de la fonction.

C'est ce qui s'en rapproche le plus :

fnSig = undefined :: [Char] -> a
fn | False = fnSig
   | True  = (* 2) . length

Sur la base de http://okmij.org/ftp/Haskell/partial-signatures.lhs via http://okmij.org/ftp/Haskell/types.html#partial-sigs

Cependant, j'aimerais une solution plus propre. Quelque chose qui communique mieux que mon intention est une restriction partielle. Quelque chose comme ceci, par exemple :

fn :: [Char] -> a
fn = (2 *) . length

Ou peut-être :

fn :: [Char] -> _
fn = (2 *) . length

Est-ce possible ?

Modifier pour plus de clarté :

@GaneshSittampalam A fait un point important dans un commentaire ci-dessous. Je cherche "une solution à mi-chemin entre l'absence totale de signature de type et la nécessité d'en donner une précise". Donc, je ne cherche pas une réponse basée sur TypeClass, je veux juste que GHC remplisse les blancs pour les types non spécifiés (ou pas complètement restreints) de ma fonction.

Editer en réponse à @WillNess

Oui, quelque chose comme ça...

fn list = 2 * length list
  where
    _ = list :: [Char]

...pourrait fonctionner, mais seulement pour les arguments, et seulement si la fonction n'est pas sans point. Existe-t-il un moyen d'appliquer cette technique aux fonctions ou aux valeurs de retour sans point ?

Editer en réponse à @Rhymoid

J'ai été inspiré, et j'ai joué avec l'idée de @Rhymoid, et j'ai trouvé ceci :

fn = (2 *) . length
  where
    _ = fn `asTypeOf` (undefined :: [Char] -> a)
    _ = fn `asTypeOf` (undefined :: a -> Int)
    _ = fn `asTypeOf` (undefined :: a -> b)
    _ = fn `asTypeOf` (undefined :: a)

Cette approche restreint également la signature de type de fn, et ne pollue aucun espace de nom.

D'ordinaire, nous n'aurions qu'une seule des asTypeOf J'ai juste ajouté plusieurs lignes pour montrer à quel point cette approche est puissante.

C'est un peu plus maladroit que ce que j'aurais souhaité, mais je pense que c'est assez intéressant de pouvoir le faire même sans support syntaxique spécifique du langage.

@Rhymoid, si vous l'aimez aussi, ajoutez-la à votre réponse :)

Answer 1

Désolé pour l'autopromotion, mais c'est exactement cette caractéristique qui est le sujet d'un article récent de Thomas Winant, étudiant en doctorat, moi-même, Frank Piessens et Tom Schrijvers, très récemment présenté par Thomas au symposium PADL 2014. Voir aquí pour le document complet. Il s'agit d'une fonctionnalité qui est déjà présente dans d'autres langages, mais l'interaction avec des fonctionnalités comme les GADTs de Haskell l'a rendue suffisamment intéressante pour que l'on travaille sur les détails.

Thomas travaille sur une implémentation pour GHC. Elle s'est encore améliorée depuis la rédaction de l'article, mais l'implémentation de la "contrainte wildcard" dans GHC est techniquement un peu plus difficile que prévu. Nous espérons pouvoir continuer à travailler sur ce sujet et contacter les développeurs de GHC pour qu'ils l'adoptent, mais cela dépendra de la volonté des gens d'avoir cette fonctionnalité en Haskell...

Answer 2

J'ai cherché un moyen de dire x s'unifie avec T '. Les solutions données par Will Ness et chi sont proches de ce que j'ai trouvé, mais il existe un moyen de le faire en Haskell 98, sans massacrer votre propre fonction.

-- Your function, without type signature.
fn = (2 *) . length

-- The type signature, without actual definition.
fnTy :: [Char] -> a
fnTy = undefined

-- If this type checks, then the type of 'fn' can be unified 
--                                      with the type of 'fnTy'.
fn_unifies_with_type :: ()
fn_unifies_with_type = let _ = fn `asTypeOf` fnTy in ()

Vous pouvez même vous contenter de

fn = (2 *) . length
  where
    _ = fn `asTypeOf` (undefined :: [Char] -> a)

Answer 3

Vous recherchez une fonctionnalité que beaucoup d'entre nous aimeraient avoir, mais que Haskell n'a pas. Ni ghc. Vous voulez une sorte de signature partielle des types. La notation suggérée pour cela est

fn :: [Char] -> _
fn = (2*) . length

Où le _ signifie "il y a un type ici, mais je ne peux pas prendre la peine de l'écrire".

Il s'agit d'une fonctionnalité très facile à mettre en œuvre (instancier _ avec des variables d'unification dans la signature), mais personne n'a pris la peine de travailler sur les détails sémantiques et l'interaction avec d'autres caractéristiques.

Answer 4

Pour spécifier seulement le type d'un argument, vous pouvez écrire quelque chose comme

fn list = 2 * length list
  where
    a :: [Char]
    a = list `asTypeOf` a

Pour qu'il soit facile de le modifier ultérieurement, par exemple,

fn list = 2 * fromIntegral (length list)
  where
    a :: [Char]
    a = list `asTypeOf` a

et que son type inféré change en conséquence :

*Main> :t fn
fn :: [Char] -> Int
*Main> :r
-- changed file reloaded
*Main> :t fn
fn :: (Num t) => [Char] -> t

Vous pourriez utiliser la même technique tordue pour spécifier le type de retour d'une fonction, peut-être définie dans le fichier sans point de contact style, mais ce n'est pas joli.

fn2 list = r
  where
    r :: Int
    r = f list
    f = (2 *) . length

Il n'est pas non plus très différent de ce que vous avez actuellement, il ne fait que séparer le code et la spécification de type.

Answer 5

Si le type de votre fn peut être automatiquement déduit sans signature, et que vous souhaitez simplement que le compilateur vérifie si le type déduit est de la bonne forme, vous pouvez utiliser quelque chose comme suit.

L'idée est d'écrire quelque chose comme

fnSig :: exists _1 _2. forall a. _1 a -> _2
fnSig = fn

sauf que Haskell ne permet pas les types existentiels ci-dessus. Cependant, les types existentiels peuvent être émulés en utilisant des types de rang supérieur comme suit :

{-# LANGUAGE RankNTypes #-}
fnSig :: (forall _1 _2.
            (forall a. _1 a -> _2)   -- your actual type, _'s are the unknowns
          ->r)->r
fnSig = \k->k fn                     -- the compiler infers _1=[] , _2=Int

-- fn :: [] a -> Int
fn = (2 *) . length

Le "truc" ci-dessus est essentiellement le même que celui utilisé par exemple dans runST.

On peut aussi déclarer un type de données existentiel ad hoc.

{-# LANGUAGE GADTs #-}
data Ex where Ex :: (forall a. _1 a -> _2) -> Ex
fnSig = Ex fn

ce qui devrait obliger le compilateur à effectuer la même vérification de type.