[Haskell-beginners] Matrix and types

mike h mike_k_houghton at yahoo.co.uk
Fri Mar 15 20:44:46 UTC 2019


Thanks.

> On 15 Mar 2019, at 13:48, Sylvain Henry <sylvain at haskus.fr> wrote:
> 
> 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 (length xs) 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 <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 <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 <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 <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 <http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners>
> _______________________________________________
> 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/89b05341/attachment-0001.html>


More information about the Beginners mailing list