Contraindre un type d'enregistrement dans Idris

Question

J'essaye d'écrire un enregistrement dans Idris mais qui a un paramètre générique qui doit être contraint par une interface. Pour normaux types d'union, je peux écrire:

data BSTree : (a : Type) -> Type where 
    Empty : Ord a => BSTree a 
    Node : Ord a => BSTree a -> a -> BSTree a 

mais je suis en train de comprendre la syntaxe pour faire la même chose, juste avec un record. J'ai essayé quelque chose comme:

record Point a where 
    constructor MkPoint : Eq a => a -> a -> Point a 
    x : a 
    y : a 

mais il ne compile pas.

Existe-t-il un moyen de le faire dans Idris?

TIA

Answer 1

Vous pouvez le faire comme ceci:

record Point a where 
    constructor MkPoint 
    x : Eq a => a 
    y : Eq a => a 

Bien en fait, vous ne devriez pas le faire. Au lieu de cela, il est préférable d'utiliser un constructeur intelligent, une autre fonction comme mkPoint : Eq a => a -> a -> MkPoint a. Dans la réalité, vous n'avez pas besoin de restreindre les types de champs pour le type de données. Lisez à propos de -XDataTypeContexts Extension Haskell.