CODEWITHSUNDEEP
haskell
Alexander Morozov
Alexander Morozov

Reputation: 593

Encoding statically known size of fixed vector as a type parameter

I would like to encode a statically known size as an arbitrary type parameter and then inside operation on values of that type to use this parameter for operations on vectors from fixed-vector package.

But I'm lost at how to use that type parameter to constrain a fixed vector to implied size.

Very simplified example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Main where

import Data.Vector.Fixed (Arity)
import qualified Data.Vector.Fixed as VF
import Data.Vector.Fixed.Unboxed

newtype Result n = Result Int

compute :: Arity n => Maybe (Result n)
compute = fmap (Result . calc) res
  where
    res = VF.replicateM (Just 1) :: Maybe (Vec n Int)
    calc = VF.sum

unpack :: Arity n => Result n -> Int
unpack (Result x) = x 

comp1 :: Int
comp1 = maybe 0 unpack r 
  where
    r = compute :: Maybe (Result 1)

main :: IO ()
main = print comp1

Gives me the following error:

src/Main.hs:18:11: error:
    • Could not deduce: Data.Vector.Fixed.Cont.Peano
                          (n2 GHC.TypeLits.+ 1)
                        ~
                        'Data.Vector.Fixed.Cont.S (Data.Vector.Fixed.Cont.Peano n2)
        arising from a use of ‘VF.replicateM’
      from the context: Arity n
        bound by the type signature for:
                   compute :: Arity n => Maybe (Result n)
        at src/Main.hs:15:1-38
    • In the expression: VF.replicateM (Just 1) :: Maybe (Vec n Int)
      In an equation for ‘res’:
          res = VF.replicateM (Just 1) :: Maybe (Vec n Int)
      In an equation for ‘compute’:
          compute
            = fmap (Result . calc) res
            where
                res = VF.replicateM (Just 1) :: Maybe (Vec n Int)
                calc = VF.sum

src/Main.hs:19:5: error:
    • Could not deduce (Data.Vector.Fixed.Cont.ArityPeano
                          (Data.Vector.Fixed.Cont.Peano n0),
                        GHC.TypeLits.KnownNat n0,
                        Data.Vector.Fixed.Cont.Peano (n0 GHC.TypeLits.+ 1)
                        ~
                        'Data.Vector.Fixed.Cont.S (Data.Vector.Fixed.Cont.Peano n0))
        arising from a use of ‘VF.sum’
      from the context: Arity n
        bound by the type signature for:
                   compute :: Arity n => Maybe (Result n)
        at src/Main.hs:15:1-38
      The type variable ‘n0’ is ambiguous
    • When instantiating ‘calc’, initially inferred to have
      this overly-general type:
        forall (v :: * -> *) a. (VF.Vector v a, Num a) => v a -> a
      NB: This instantiation can be caused by the monomorphism restriction.
      In an equation for ‘compute’:
          compute
            = fmap (Result . calc) res
            where
                res = VF.replicateM (Just 1) :: Maybe (Vec n Int)
                calc = VF.sum

I suspect that GHC does not see any connection between n in Result n and n in :: Maybe (Vec n Int).

Maybe I'm doing it all wrong.

What I really have is a family of types, for each natural number from 1 to N. And I need to, for example, declare each type an instance of some class and use fixed vector for that number inside that class method. So, store a natural number as a type parameter, then, in some function bound only by that type, extract that number and use it to operate internally on fixed vectors by that size.

Upvotes: 2

Views: 167

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33389

You're almost there!. In the body compute there is a reference to the type variable n, but to do that actually requires an extension: ScopedTypeVariables.

{-# LANGUAGE ScopedTypeVariables #-}

           -- Must be explicitly bound...
compute :: forall n. Arity n => Maybe (Result n)
compute = fmap (Result . calc) res
  where
    res = VF.replicateM (Just 1) :: Maybe (Vec n Int)  -- ... so it can be referred to here
    calc = VF.sum

Upvotes: 2

Related Questions