J'explore des familles de types dans Haskell, en essayant d'établir la complexité des fonctions de niveau que je peux définir. Je veux définir une version de type fermé niveau de mod, quelque chose comme ceci:Contraintes dans les instances de familles de types

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-} 
import GHC.TypeLits 

type family Mod (m :: Nat) (n :: Nat) :: Nat where 
    n <= m => Mod m n = Mod (m - n) n 
    Mod m n = m

Cependant, le compilateur (GHC 7.10.2) rejette cela, comme la contrainte dans la première équation est pas autorisée. Comment les gardes au niveau de la valeur se traduisent-ils au niveau du type? Est-ce encore possible à Haskell actuellement?

2016-05-31 prophet-on-that

Peut-être qu'il y a une fonction de niveau de type 'If'? Je pense que j'ai vu ça utilisé quelque part, mais je ne suis pas un expert en bibliothéconomie ... – chi

Merci, vous avez absolument raison, 'If' existe dans [Data.Type.Bool] (https://hackage.haskell.org /package/base/docs/Data-Type-Bool.html). –

Suite à cela, j'ai réussi à réécrire 'Mod' en utilisant le niveau de type' If', qui a été compilé avec succès. Cependant, toute tentative de réduction d'un terme du formulaire 'Mod m n' aboutit à une exception de dépassement de pile. Le fait de peaufiner l'option _-freduction-depth_ m'a montré que GHC donnait la priorité à l'expansion de la partie «m - n» de l'expression, sans se rendre compte que cela pourrait ne jamais être possible. Je vais devoir regarder plus loin dans l'extension _DataKinds_ pour mieux comprendre le comportement. –

Pas une réponse (je ne pense pas qu'il y en ait encore une possible), mais pour le bénéfice d'autres personnes (comme moi) essayant de retracer les étapes OP dans les commentaires. Les compilations suivantes, mais en l'utilisant rapidement entraîne un débordement de pile.

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-} 
import GHC.TypeLits 
import Data.Type.Bool 

type family Mod (m :: Nat) (n :: Nat) :: Nat where 
    Mod m n = If (n <=? m) (Mod (m - n) n) m

La raison est que If lui-même est juste une famille de type régulier et le comportement des familles de type-est de commencer par l'expansion de leurs arguments de type (désireux dans un sens) avant d'utiliser ceux du côté droit. Le résultat malheureux dans ce cas est que Mod (m - n) n est élargi même si n <=? m est faux, d'où le débordement de la pile.

Pour exactement la même raison, les opérateurs logiques dans Data.Type.Bool ne court-circuitent pas. Compte tenu

type family Bottom :: Bool where Bottom = Bottom

Nous pouvons voir que False && Bottom et True || Bottom raccrochiez tous les deux.

EDIT

Juste au cas où l'OP est juste intéressé par une famille de type avec le comportement requis (et pas seulement le problème plus général d'avoir des gardes dans les familles de type), il est un moyen d'exprimer Mod en d'une manière qui se termine:

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-} 
import GHC.TypeLits 

type Mod m n = Mod1 m n 0 m 

type family Mod1 (m :: Nat) (n :: Nat) (c :: Nat) (acc :: Nat) :: Nat where 
    Mod1 m n n acc = Mod1 m n 0 m 
    Mod1 0 n c acc = acc 
    Mod1 m n c acc = Mod1 (m - 1) n (c + 1) acc

Source

2016-07-28 21:55:09 Alec

Contraintes dans les instances de familles de types

Répondre

EDIT

Questions connexes