TP | 27 Apr 21:33 2013
Picon

partially applied data constructor and corresponding type

Hello,

I ask myself if there is a way to do the following.
Imagine that I have a dummy type:

data Tensor = TensorVar Int String

where the integer is the order, and the string is the name of the tensor.
I would like to make with the constructor TensorVar a type "Vector", such 
that, in "pseudo-language":

data Vector = TensorVar 1 String

Because a vector is a tensor of order 1.

Is this possible? I have tried type synonyms and newtypes without any success.

Thanks a lot,

TP
Yury Sulsky | 27 Apr 22:16 2013
Picon

Re: partially applied data constructor and corresponding type

Hi TP,

Are you looking to use a phantom types here? Here's an example:

data One
data Two

data Tensor ndims a = Tensor { dims :: [Int], items :: [a] }
type Vector = Tensor One
type Matrix = Tensor Two

etc.


On Sat, Apr 27, 2013 at 3:33 PM, TP <paratribulations <at> free.fr> wrote:
Hello,

I ask myself if there is a way to do the following.
Imagine that I have a dummy type:

data Tensor = TensorVar Int String

where the integer is the order, and the string is the name of the tensor.
I would like to make with the constructor TensorVar a type "Vector", such
that, in "pseudo-language":

data Vector = TensorVar 1 String

Because a vector is a tensor of order 1.

Is this possible? I have tried type synonyms and newtypes without any success.

Thanks a lot,

TP

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
TP | 27 Apr 23:35 2013
Picon

Re: partially applied data constructor and corresponding type

Thanks Yury,

 

The problem with this solution is that if I have written a method for the Tensor type (for example a method of a typeclass of which Tensor is an instance) that uses the order of the tensor (your "ndims") in a general way, I cannot reuse it easily for a vector defined like that.

 

In fact, my problem is to be able to define:

* from my type "Tensor", a type "Vector", by specifying that the dimension must be one to have a "Vector" type.

* from my constructor "TensorVar", a constructor "VectorVar", which corresponds to TensorVar with the integer equal to 1.

 

The idea is to avoid duplicating code, by reusing the tensor type and data constructor. At some place in my code, in some definition (say, of a vector product), I want vectors and not more general tensors.

 

TP

 

On Saturday, April 27, 2013 16:16:49 Yury Sulsky wrote:

Hi TP,


Are you looking to use a phantom types here? Here's an example:


data One

data Two


data Tensor ndims a = Tensor { dims :: [Int], items :: [a] }

type Vector = Tensor One

type Matrix = Tensor Two


etc.



On Sat, Apr 27, 2013 at 3:33 PM, TP <paratribulations <at> free.fr> wrote:

Hello,

I ask myself if there is a way to do the following.
Imagine that I have a dummy type:

data Tensor = TensorVar Int String

where the integer is the order, and the string is the name of the tensor.
I would like to make with the constructor TensorVar a type "Vector", such
that, in "pseudo-language":

data Vector = TensorVar 1 String

Because a vector is a tensor of order 1.

Is this possible? I have tried type synonyms and newtypes without any success.

Thanks a lot,

TP

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Stephen Tetley | 28 Apr 08:58 2013
Picon

Re: partially applied data constructor and corresponding type

What you probably want are type level integers (naturals)

Yury Sulsky used them in the message above - basically you can't use
literal numbers 1,2,3,... etc as they are values of type Int (or
Integer, etc...) instead you have to use type level numbers:

data One
data Two

Work is ongoing for type level numbers in GHC and there are user
libraries on Hackage so there is a lot of work to crib from.
TP | 29 Apr 08:55 2013
Picon

Re: partially applied data constructor and corresponding type

Thanks for pointing to "type level integers". With that I have found:

http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5/Number_Param_Types

For example:

-------------------------------
data Zero = Zero
data Succ a = Succ a

class Card c where
    c2num:: c -> Integer

    cpred::(Succ c) -> c
    cpred = undefined

instance Card Zero where 
    c2num _ = 0

instance (Card c) => Card (Succ c) where
    c2num x = 1 + c2num (cpred x)

main = do

putStrLn $ show $ c2num (Succ (Succ Zero))
-------------------------------

I will continue to examine the topic in the following days, according to my 
needs.

Thanks a lot,

TP

On Sunday, April 28, 2013 07:58:58 Stephen Tetley wrote:
> What you probably want are type level integers (naturals)
> 
> Yury Sulsky used them in the message above - basically you can't use
> literal numbers 1,2,3,... etc as they are values of type Int (or
> Integer, etc...) instead you have to use type level numbers:
> 
> data One
> data Two
> 
> Work is ongoing for type level numbers in GHC and there are user
> libraries on Hackage so there is a lot of work to crib from.
Richard Eisenberg | 29 Apr 14:19 2013

Re: partially applied data constructor and corresponding type

There's a lot of recent work on GHC that might be helpful to you. Is it possible for your application to use GHC
7.6.x? If so, you could so something like this:

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Nat = Zero | Succ Nat

type One = Succ Zero
type Two = Succ One
type Three = Succ Two

-- connects the type-level Nat with a term-level construct
data SNat :: Nat -> * where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)

zero = SZero
one = SSucc zero
two = SSucc one
three = SSucc two

data Tensor (n :: Nat) a = MkTensor { dims :: SNat n, items :: [a] }

type Vector = Tensor One
type Matrix = Tensor Two

mkVector :: [a] -> Vector a
mkVector v = MkTensor { dims = one, items = v }

vector_prod :: Num a => Vector a -> Vector a
vector_prod (MkTensor { items = v }) = ...

specializable :: Tensor n a -> Tensor n a
specializable (MkTensor { dims = SSucc SZero, items = vec }) = ...
specializable (MkTensor { dims = SSucc (SSucc SZero), items = mat }) = ...

This is similar to other possible approaches with type-level numbers, but it makes more use of the newer
features of GHC that assist with type-level computation. Unfortunately, there are no "constructor
synonyms" or "pattern synonyms" in GHC, so you can't pattern match on "MkVector" or something similar in
specializable. But, the pattern matches in specializable are GADT pattern-matches, and so GHC knows
what the value of n, the type variable, is on the right-hand sides. This will allow you to write and use
instances of Tensor defined only at certain numbers of dimensions.

I hope this is helpful. Please write back if this technique is unclear!

Richard

On Apr 29, 2013, at 2:55 AM, TP <paratribulations <at> free.fr> wrote:

> Thanks for pointing to "type level integers". With that I have found:
> 
> http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5/Number_Param_Types
> 
> For example:
> 
> -------------------------------
> data Zero = Zero
> data Succ a = Succ a
> 
> class Card c where
>    c2num:: c -> Integer
> 
>    cpred::(Succ c) -> c
>    cpred = undefined
> 
> instance Card Zero where 
>    c2num _ = 0
> 
> instance (Card c) => Card (Succ c) where
>    c2num x = 1 + c2num (cpred x)
> 
> main = do
> 
> putStrLn $ show $ c2num (Succ (Succ Zero))
> -------------------------------
> 
> I will continue to examine the topic in the following days, according to my 
> needs.
> 
> Thanks a lot,
> 
> TP
> 
> On Sunday, April 28, 2013 07:58:58 Stephen Tetley wrote:
>> What you probably want are type level integers (naturals)
>> 
>> Yury Sulsky used them in the message above - basically you can't use
>> literal numbers 1,2,3,... etc as they are values of type Int (or
>> Integer, etc...) instead you have to use type level numbers:
>> 
>> data One
>> data Two
>> 
>> Work is ongoing for type level numbers in GHC and there are user
>> libraries on Hackage so there is a lot of work to crib from.
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
TP | 29 Apr 23:26 2013
Picon

Re: partially applied data constructor and corresponding type

Thanks a lot for your message.
I can use a recent version of GHC 7.6.x (I will install the last version of 
Kubuntu for that purpose).
However, it will take me some time to understand correctly this code (e.g. I 
do not know "data kinds"), I will go back to you if I encounter difficulties.

Thanks,

TP

On Monday, April 29, 2013 08:19:43 Richard Eisenberg wrote:
> There's a lot of recent work on GHC that might be helpful to you. Is it
> possible for your application to use GHC 7.6.x? If so, you could so
> something like this:
> 
> {-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
> 
> data Nat = Zero | Succ Nat
> 
> type One = Succ Zero
> type Two = Succ One
> type Three = Succ Two
> 
> -- connects the type-level Nat with a term-level construct
> data SNat :: Nat -> * where
>   SZero :: SNat Zero
>   SSucc :: SNat n -> SNat (Succ n)
> 
> zero = SZero
> one = SSucc zero
> two = SSucc one
> three = SSucc two
> 
> data Tensor (n :: Nat) a = MkTensor { dims :: SNat n, items :: [a] }
> 
> type Vector = Tensor One
> type Matrix = Tensor Two
> 
> mkVector :: [a] -> Vector a
> mkVector v = MkTensor { dims = one, items = v }
> 
> vector_prod :: Num a => Vector a -> Vector a
> vector_prod (MkTensor { items = v }) = ...
> 
> specializable :: Tensor n a -> Tensor n a
> specializable (MkTensor { dims = SSucc SZero, items = vec }) = ...
> specializable (MkTensor { dims = SSucc (SSucc SZero), items = mat }) = ...
> 
> 
> This is similar to other possible approaches with type-level numbers, but it
> makes more use of the newer features of GHC that assist with type-level
> computation. Unfortunately, there are no "constructor synonyms" or "pattern
> synonyms" in GHC, so you can't pattern match on "MkVector" or something
> similar in specializable. But, the pattern matches in specializable are
> GADT pattern-matches, and so GHC knows what the value of n, the type
> variable, is on the right-hand sides. This will allow you to write and use
> instances of Tensor defined only at certain numbers of dimensions.
> 
> I hope this is helpful. Please write back if this technique is unclear!
> 
> Richard
TP | 18 May 23:48 2013
Picon

Re: partially applied data constructor and corresponding type

Richard Eisenberg wrote:

> There's a lot of recent work on GHC that might be helpful to you. Is it
> possible for your application to use GHC 7.6.x? If so, you could so
> something like this:
> 
> {-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
> 
> data Nat = Zero | Succ Nat
> 
> type One = Succ Zero
> type Two = Succ One
> type Three = Succ Two
> 
> -- connects the type-level Nat with a term-level construct
> data SNat :: Nat -> * where
>   SZero :: SNat Zero
>   SSucc :: SNat n -> SNat (Succ n)
> 
> zero = SZero
> one = SSucc zero
> two = SSucc one
> three = SSucc two
> 
> data Tensor (n :: Nat) a = MkTensor { dims :: SNat n, items :: [a] }
> 
> type Vector = Tensor One
> type Matrix = Tensor Two
> 
> mkVector :: [a] -> Vector a
> mkVector v = MkTensor { dims = one, items = v }
> 
> vector_prod :: Num a => Vector a -> Vector a
> vector_prod (MkTensor { items = v }) = ...
> 
> specializable :: Tensor n a -> Tensor n a
> specializable (MkTensor { dims = SSucc SZero, items = vec }) = ...
> specializable (MkTensor { dims = SSucc (SSucc SZero), items = mat }) = ...
> 
> 
> This is similar to other possible approaches with type-level numbers, but
> it makes more use of the newer features of GHC that assist with type-level
> computation. Unfortunately, there are no "constructor synonyms" or
> "pattern synonyms" in GHC, so you can't pattern match on "MkVector" or
> something similar in specializable. But, the pattern matches in
> specializable are GADT pattern-matches, and so GHC knows what the value of
> n, the type variable, is on the right-hand sides. This will allow you to
> write and use instances of Tensor defined only at certain numbers of
> dimensions.
> 
> I hope this is helpful. Please write back if this technique is unclear!

Thanks a lot! Those days I have read about "DataKinds" extension (with help 
of Haskell-Cafe guys), and now I am able to understand your code. The 
technique to connect the type-level and term-level integers allows to 
duplicate information (duplicate information needed because of my more or 
less clear requirements in my previous posts), but in a safe way (i.e. with 
no copy/paste error): if I change "one" in "two" in the definition of the 
smart constructor mkVector, I obtain an error, as expected because of the 
use of type variable n on both sides of the equality in Tensor type 
definition (and then we understand why the type constructor SNat has been 
introduced).

This is a working example (this is not exactly what I will do at the end, 
but it is very instructive! One more time, thanks!):
--------------------------------------
{-# LANGUAGE DataKinds, GADTs, KindSignatures, StandaloneDeriving #-}

data Nat = Zero | Succ Nat

type One = Succ Zero
type Two = Succ One
type Three = Succ Two

-- connects the type-level Nat with a term-level construct
data SNat :: Nat -> * where
    SZero :: SNat Zero
    SSucc :: SNat n -> SNat (Succ n)

deriving instance Show (SNat a)

zero = SZero
one = SSucc zero
two = SSucc one
three = SSucc two

data Tensor (n :: Nat) a = MkTensor { order :: SNat n, items :: [a] }
    deriving Show

type Vector = Tensor One
type Matrix = Tensor Two

mkVector :: [a] -> Vector a
mkVector v = MkTensor { order = one, items = v }

-- some dummy operation defined between two Vectors (and not other order
-- tensors), which results in a Vector.
some_operation :: Num a => Vector a -> Vector a -> Vector a
some_operation (MkTensor { items = v1 }) (MkTensor { items = v2 }) =
    mkVector (v1 ++ v2)

main = do

let va = mkVector ([1,2,3] :: [Integer])
let vb = mkVector ([4,5,6] :: [Integer])

print $ some_operation va vb
print $ order va
print $ order vb
---------------------------------

Gmane