hypercuboidの応用例

Question

私はを使って、HaskellのAPLに似たプログラミングを行っています。私は、それが完全に実行可能であると述べているが、hypercuboidデータ型のためにApplicativeインスタンスを定義することに固執した。簡略化された例は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 
-} 

（例えば、リストの長さタイプインデックス）Vector n aタイプ約Applicativeインスタンスが知られているものを想起Iは約purereplicateとして（与えられた値のn進複製）考えてみました。しかし、これは、私が知る限り、ハスケルでは使用できないタイプレベルのケース（例：pure a = case fs of '[] -> Scalar a; (f ': gs) -> <something using the fact that Applicative f>）が必要なようです。

Answer 1

ます（「タイプレベルのケース」の一種である。）Hyper '[]とHyper (f ': fs)のための個別のインスタンスを定義することができ

あなたはそれがparametricityに違反するので、あなたが望むどのように動作する単一のインスタンスApplicative (Hyper fs)を定義することはできません。確かに私はisScalar :: Hyper fs -> Boolを明白な方法で定義することができます。 isScalar (pure())とは何ですか？

（ここで、あなたはHyper (f ': fs)場合にf上の制約が必要になります理由とにかく単一インスタンスApplicative (Hyper fs)を定義することができません。）

Answer 2

あなたはタイプレベルのケースを行うことができません、タイプレベルの情報を確認する価値レベルのケースを実行できます。このような

data Shapely (fs :: [* -> *]) where 
    ShZ :: Shapely '[] 
    ShS :: (Dim f) => Shapely 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 shapely 

この方法で型クラス、実際にあなたが望むようにパターンマッチングを行うことができます値レベルの情報を提供しています。私。あなたは今ではfsは、タイプレベルで'[]に書き換えますとScalar xが今受け入れられ、ShZパターンマッチがそのfs ~ '[]明らか

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 

のようなものを定義することができます。 ShSのケースでは、同様に動作します。

Prismもので、ここで、ちょうどShapely fs（まあ、それはできますが、not in a very nice way）から推定することはできませんSShapely fs制約が改善エンコーディングされているので、しかし、これは本当に、チェックを入力しません：

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をShapelyに変更しました。Shapely fsは最初に届きませんが、代わりにSShapely fsという制約があります。この場合、Shapely fsは常に復元できます。これで、タイプが適切に一致します。

The code。