12
L'extension DataKinds promeut des "valeurs" (c'est-à-dire des constructeurs) en types. Par exemple True et False deviennent des types distincts de type Bool. Ce que je voudrais faire est le contraire, c'est-à-dire rétrograder les types en valeurs. Une fonction avec cette signature serait bien:Rétrogradation type (par opposition à la promotion Kind)
demote :: Proxy (a :: t) -> t
je peux réellement faire, par exemple pour Bool:
class DemoteBool (a :: Bool) where
demoteBool :: Proxy (a :: Bool) -> Bool
instance DemoteBool True where
demoteBool _ = True
instance DemoteBool False where
demoteBool _ = False
Cependant, je dois rédiger des cas pour tout type que je veux rétrograder à sa valeur. Y a-t-il une façon plus agréable de faire cela qui n'implique pas tant de passe-partout?
La raison pour laquelle vous devez le faire manuellement est la partialité. Étant donné un niveau de type 'b :: Bool', vous ne savez pas avec certitude s'il s'agit de' True' ou 'False'. Il pourrait s'agir d'un [type coincé] (https://typesandkinds.wordpress.com/2015/09/09/what-are-type-families/). Un singleton prouve que son type n'est pas bloqué. La dépendance de Haskell aidera un peu dans ce cas particulier, car 'True' et 'True' seront la même chose, mais il y a toujours des problèmes inévitables de partialité. –
@BenjaminHodgson fait l'aide 'TypeInType' existant ici ou est-ce sans rapport? – porges
Ce serait amusant si des champs stricts ne pouvaient pas contenir de types bloqués, tout comme un champ strict ne peut pas contenir de bas. Je veux juste être en mesure d'étendre la portée de 'a ::! Bool' et l'utiliser dans le code :) – porges