[Haskell-beginners] Matrix and types
Sylvain Henry
sylvain at haskus.fr
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>
More information about the Beginners
mailing list