[Haskell-beginners] Matrix and types

Fri Mar 15 13:48:06 UTC 2019

Hi,

The problem is that Haskell lists don't carry their length in their type 
hence you cannot enforce their length at compile time. But you can 
define your M this way instead:

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}

import GHC.TypeNats
import Data.Proxy

data M (n :: Nat) a where
    MNil  :: M 0 a
    MCons :: a -> M (n-1) a -> M n a

infixr 5 `MCons`

toList :: M k a -> [a]
toList MNil         = []
toList (MCons a as) = a:toList as

instance (KnownNat n, Show a) => Show (M n a) where
    show xs = mconcat
       [ "M @"
       , show (natVal (Proxy :: Proxy n))
       , " "
       , show (toList xs)
       ]

--t2 :: M 2 Integer
t2 = 1 `MCons` 2 `MCons` MNil

--t3 :: M 3 Integer
t3 = 1 `MCons` 2 `MCons` 3 `MCons` MNil

zipM :: (a -> b -> c) -> M n a -> M n b -> M n c
zipM _f MNil         MNil         = MNil
zipM  f (MCons a as) (MCons b bs) = MCons (f a b) (zipM f as bs)

fx :: Num a => M n a -> M n a -> M n a
fx = zipM (+)

Test:

 > t2
M @2 [1,2]
 > fx t2 t2
M @2 [2,4]
 > fx t2 t3

<interactive>:38:7: error:
     • Couldn't match type ‘3’ with ‘2’
       Expected type: M 2 Integer
         Actual type: M 3 Integer

Cheers,
Sylvain

On 15/03/2019 13:57, mike h wrote:
>
> Hi Frederic,
>
> Yeh, my explanation is a bit dubious :)
> What I’m trying to say is:
> Looking at the type M (n::Nat)
> If I want an M 2  of Ints say,  then I need to write the function with 
> signature
>
>  f :: M 2 Int
>
> If I want a M 3 then I need to explicitly write the function with 
> signature
> M 3 Int
>
> and so on for every possible instance that I might want.
>
> What I would like to do is have just one function that is somehow 
> parameterised to create the M tagged with the required value of (n::Nat)
> In pseudo Haskell
>
> create :: Int -> [Int] -> M n
> create size ns = (M ns) ::  M size Int
>
> where  its trying to coerce (M ns) into the type (M size Int) where 
> size is an Int but needs to be a Nat.
>
> It’s sort of like parameterising the signature of the function.
>
> Thanks
>
> Mike
>
>> On 15 Mar 2019, at 11:37, Frederic Cogny <frederic.cogny at gmail.com 
>> <mailto:frederic.cogny at gmail.com>> wrote:
>>
>> I'm not sure I understand your question Mike.
>> Are you saying createIntM behaves as desired but the data constructor 
>> M could let you build a data M with the wrong type. for instance M 
>> [1,2] :: M 1 Int ?
>>
>> If that is your question, then one way to handle this is to have a 
>> separate module where you define the data type and the proper 
>> constructor (here M and createIntM) but where you do not expose the 
>> type constructor. so something like
>>
>> module MyModule
>>   ( M -- as opposed to M(..) to not expose the type constructor
>> , createIntM
>>   ) where
>>
>> Then, outside of MyModule, you can not create an incorrect lentgh 
>> annotated list since the only way to build it is through createIntM
>>
>> Does that make sense?
>>
>> On Thu, Mar 14, 2019 at 4:19 PM mike h <mike_k_houghton at yahoo.co.uk 
>> <mailto:mike_k_houghton at yahoo.co.uk>> wrote:
>>
>>     Hi,
>>     Thanks for the pointers. So I’ve got
>>
>>     data M (n :: Nat) a = M [a] deriving Show
>>
>>     t2 :: M 2 Int
>>     t2  = M [1,2]
>>
>>     t3 :: M 3 Int
>>     t3 = M [1,2,3]
>>
>>     fx :: Num a => M n a -> M n a -> M n a
>>     fx (M xs) (M ys) = M (zipWith (+) xs ys)
>>
>>     and having
>>     g = fx t2 t3
>>
>>     won’t compile. Which is what I want.
>>     However…
>>
>>     t2::M 2 Int
>>     t2 =M [1,2]
>>
>>     is ‘hardwired’ to 2 and clearly I could make t2 return  a list of
>>     any length.
>>     So what I then tried to look at was a general function that would
>>     take a list of Int and create the M type using the length of
>>     the supplied list.
>>     In other words if I supply a list, xs, of length n then I wan’t
>>      M n xs
>>     Like this
>>
>>     createIntM xs = (M xs) ::M (lengthxs) Int
>>
>>     which compile and has type
>>     λ-> :t createIntM
>>     createIntM :: [Int] -> M (length xs) Int
>>
>>     and all Ms created using createIntM  have the same type
>>     irrespective of the length of the supplied list.
>>
>>     What’s the type jiggery I need or is this not the right way to go?
>>
>>     Thanks
>>
>>     Mike
>>
>>
>>
>>
>>>     On 14 Mar 2019, at 13:12, Frederic Cogny
>>>     <frederic.cogny at gmail.com <mailto:frederic.cogny at gmail.com>> wrote:
>>>
>>>     The (experimental) Static module of hmatrix seems (I've used the
>>>     packaged but not that module) to do exactly that:
>>>     http://hackage.haskell.org/package/hmatrix-0.19.0.0/docs/Numeric-LinearAlgebra-Static.html
>>>
>>>
>>>
>>>
>>>     On Thu, Mar 14, 2019, 12:37 PM Francesco Ariis <fa-ml at ariis.it
>>>     <mailto:fa-ml at ariis.it>> wrote:
>>>
>>>         Hello Mike,
>>>
>>>         On Thu, Mar 14, 2019 at 11:10:06AM +0000, mike h wrote:
>>>         > Multiplication of two matrices is only defined when the
>>>         the number of columns in the first matrix
>>>         > equals the number of rows in the second matrix. i.e. c1 == r2
>>>         >
>>>         > So when writing the multiplication function I can check
>>>         that  c1 == r2 and do something.
>>>         > However what I really want to do, if possible, is to have
>>>         the compiler catch the error.
>>>
>>>         Type-level literals [1] or any kind of similar trickery
>>>         should help you
>>>         with having matrices checked at compile-time.
>>>
>>>         [1]
>>>         https://downloads.haskell.org/~ghc/7.10.1/docs/html/users_guide/type-level-literals.html
>>>         _______________________________________________
>>>         Beginners mailing list
>>>         Beginners at haskell.org <mailto:Beginners at haskell.org>
>>>         http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>>>
>>>     -- 
>>>     Frederic Cogny
>>>     +33 7 83 12 61 69
>>>     _______________________________________________
>>>     Beginners mailing list
>>>     Beginners at haskell.org <mailto:Beginners at haskell.org>
>>>     http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>>
>> -- 
>> Frederic Cogny
>> +33 7 83 12 61 69
>
>
> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20190315/f6c93d5a/attachment-0001.html>