Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Applicative instance for hypercuboid

I'm working through extended abstract by Prof. J.Gibbons on APL-like programming in Haskell. I stuck with defining Applicative instance for hypercuboid datatype, though the paper states that it is perfectly doable. Simplified example is 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
-}

Recalling what is known about Applicative instance for Vector n a type (e.g. a list type-indexed by its length) I tried to think about pure as replicate (n-ary replication of a given value). But seems like this requires typelevel case (e.g. pure a = case fs of '[] -> Scalar a; (f ': gs) -> <something using the fact that Applicative f>) which is not avalilable in Haskell as far as I know.

like image 503
Artem Pelenitsyn Avatar asked Mar 11 '23 11:03

Artem Pelenitsyn


1 Answers

You can define separate instances for Hyper '[] and Hyper (f ': fs) (which is a sort of "type-level case".)

You can't define a single instance Applicative (Hyper fs) that behaves how you want because it would violate parametricity. Certainly I can define isScalar :: Hyper fs -> Bool in the obvious way; then what is isScalar (pure ())?

(Here, you wouldn't be able to define a single instance Applicative (Hyper fs) anyways for the reason that you will need a constraint on f in the Hyper (f ': fs) case.)

like image 75
Reid Barton Avatar answered Mar 21 '23 04:03

Reid Barton