Instance d'application pour l'hypercubide

Question

Je travaille sur extended abstract by Prof. J.Gibbons sur la programmation de type APL dans Haskell. Je me suis contenté de définir Applicative instance pour le type de données hypercuboid, bien que le document indique que c'est parfaitement faisable. L'exemple simplifié est as follows.

{-# LANGUAGE KindSignatures, GADTs, TypeFamilies, TypeOperators, MultiParamTypeClasses, DataKinds #-} 

import Control.Applicative 
import Data.Traversable (Traversable) 

class (Applicative f, Traversable f) => Dim f 

class Shapely (fs :: [* -> *]) 
instance Shapely '[] 
instance (Dim f, Shapely fs) => Shapely (f ': fs) 

------------------------------------- 
--   Hypercuboid datatype 
------------------------------------- 
data Hyper :: [* -> *] -> * -> * where 
    Scalar :: a -> Hyper '[] a 
    Prism :: (Dim f, Shapely fs) => 
       Hyper fs (f a) -> Hyper (f ': fs) a 

instance Functor (Hyper fs) where 
    fmap f (Scalar a) = Scalar $ f a 
    fmap f (Prism p) = Prism $ fmap (fmap f) p 

instance Applicative (Hyper fs) where 
    pure a = undefined 
{- `pure a = Scalar a` gives: 
      Couldn't match type ‘fs’ with ‘'[]’ 
        ‘fs’ is a rigid type variable bound by 
         the instance declaration 
      Expected type: Hyper fs a 
       Actual type: Hyper '[] a 
-} 

Rappelant ce qui est connu Applicative par exemple pour le type Vector n a (par exemple une indexation de type liste par sa longueur) J'ai essayé de penser à pure comme replicate (réplication n-aire d'une valeur donnée). Mais il semble que cela nécessite un cas typique (par exemple pure a = case fs of '[] -> Scalar a; (f ': gs) -> <something using the fact that Applicative f>) qui n'est pas disponible chez Haskell autant que je sache.

Answer 1

Vous pouvez définir des instances distinctes pour Hyper '[] et Hyper (f ': fs) (ce qui est une sorte de « cas de niveau de type ».)

Vous ne pouvez pas définir une seule instance Applicative (Hyper fs) qui se comporte comment vous voulez parce que cela serait contraire à paramétricité . Certes, je peux définir isScalar :: Hyper fs -> Bool de façon évidente; alors qu'est-ce que isScalar (pure())?

(Ici, vous ne seriez pas en mesure de définir une seule instance Applicative (Hyper fs) de toute façon pour la raison que vous aurez besoin d'une contrainte sur f dans le cas Hyper (f ': fs).)

Answer 2

Vous ne pouvez pas faire cas de niveau du type, mais vous pouvez faire un cas au niveau de la valeur qui réifie les informations au niveau du type. Normalement, vous définissez un singleton comme ceci:

data Shapely (fs :: [* -> *]) where 
    ShZ :: Shapely '[] 
    ShS :: (Dim f) => Shapely fs -> Shapely (f ': fs) 

et une classe de type comme ceci:

class SShapely (fs :: [* -> *]) where 
    shapely :: Shapely fs 

instance SShapely '[] where 
    shapely = ShZ 

instance (Dim f, SShapely fs) => SShapely (f ': fs) where 
    shapely = ShS shapely 

De cette façon, le type de classe effectivement fournir des informations au niveau de valeur qui permet d'effectuer la correspondance de modèles comme vous voulez. C'est à dire. vous pouvez maintenant définir quelque chose comme

pureSh :: Shapely fs -> a -> Hyper fs a 
pureSh ShZ x = Scalar x 
pureSh (ShS s) x = Prism (pureSh s (pure x)) 

instance SShapely fs => Applicative (Hyper fs) where 
    pure = pureSh shapely 

Le match de modèle ShZ révèle que fs ~ '[], si fs est réécrite à '[] au niveau du type et Scalar x est maintenant accepté. Dans le cas ShS, les choses fonctionnent de manière similaire.

Toutefois, cela ne tapez pas vraiment vérifier, parce que Prism a aussi la contrainte SShapely fs qui ne peut être déduit de tout Shapely fs (bien, il peut, mais not in a very nice way), alors voici un meilleur encodage:

data Shapely (fs :: [* -> *]) where 
    ShZ :: Shapely '[] 
    ShS :: (Dim f, SShapely fs) => Shapely (f ': fs) 

class SShapely (fs :: [* -> *]) where 
    shapely :: Shapely fs 

instance SShapely '[] where 
    shapely = ShZ 

instance (Dim f, SShapely fs) => SShapely (f ': fs) where 
    shapely = ShS 

pureSh :: Shapely fs -> a -> Hyper fs a 
pureSh ShZ x = Scalar x 
pureSh ShS x = Prism (pureSh shapely (pure x)) 

instance SShapely fs => Applicative (Hyper fs) where 
    pure = pureSh shapely 

ShS dans Shapely maintenant ne reçoit pas un Shapely fs de premier ordre, mais a la contrainte SShapely fs à la place, à partir de laquelle un Shapely fs peut toujours être récupéré. Maintenant, les types correspondent correctement.

The code.