[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