Structural restrictions in type constructor

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
16 messages Options
Reply | Threaded
Open this post in threaded view
|

Structural restrictions in type constructor

Matt Williams-2

Dear All,

I wonder if/ how this is possible?

I have a constructor which takes 2 pairs of type t).

However, I want to ensure that the pairs are matched:

MyP = MyP (t, t) (t, t)

But where the first pair contains the same elements as the second, but reversed in order.

Any help much appreciated.

BW,
Matt


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Martin Vlk
I would think that it is not possible to use types to constrain the
values of data. I.e. type signature can be only used to constraint
types, not values.

But I am a beginner myself, so see if someone more experienced can shed
light here.

Martin


Matt Williams:

> Dear All,
>
> I wonder if/ how this is possible?
>
> I have a constructor which takes 2 pairs of type t).
>
> However, I want to ensure that the pairs are matched:
>
> MyP = MyP (t, t) (t, t)
>
> But where the first pair contains the same elements as the second, but
> reversed in order.
>
> Any help much appreciated.
>
> BW,
> Matt
>
>
>
> _______________________________________________
> Beginners mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Imants Cekusins
we could use pattern matched constructor:

module PairsMatched where

data MyP t = MyP (t,t)(t,t) deriving Show


myP_ctor:: Eq t => (t,t)->(t,t)->MyP t
myP_ctor (a1,a2) (a3,a4)
   | a1 == a4 && a2 == a3 = MyP (a1,a2) (a3,a4)
   | otherwise = error "mismatched pairs"
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Martin Vlk
But this is checking the values in the implementation, not a type level
build time guarantee, isn't it?

M

Imants Cekusins:

> we could use pattern matched constructor:
>
> module PairsMatched where
>
> data MyP t = MyP (t,t)(t,t) deriving Show
>
>
> myP_ctor:: Eq t => (t,t)->(t,t)->MyP t
> myP_ctor (a1,a2) (a3,a4)
>    | a1 == a4 && a2 == a3 = MyP (a1,a2) (a3,a4)
>    | otherwise = error "mismatched pairs"
> _______________________________________________
> Beginners mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
>
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Imants Cekusins
> But this is checking the values in the implementation, not a type level
build time guarantee, isn't it?

yep, correct. Could be caught by unit tests though :-P
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

emacstheviking
It *could* be done and might already have been done... I seem to recall a few months back somebody asked for a similar feature using one of the vector libraries, to limit one of the input vectors to a fixed length?

You'd have to dig through the list archives though...

On 22 June 2015 at 12:36, Imants Cekusins <[hidden email]> wrote:
> But this is checking the values in the implementation, not a type level
build time guarantee, isn't it?

yep, correct. Could be caught by unit tests though :-P
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Matt Williams-2
OK, I think this is clearly well beyond my level!

Will insert some manual checking.

Thanks,
Matt

On 22 June 2015 at 14:51, emacstheviking <[hidden email]> wrote:
It *could* be done and might already have been done... I seem to recall a few months back somebody asked for a similar feature using one of the vector libraries, to limit one of the input vectors to a fixed length?

You'd have to dig through the list archives though...

On 22 June 2015 at 12:36, Imants Cekusins <[hidden email]> wrote:
> But this is checking the values in the implementation, not a type level
build time guarantee, isn't it?

yep, correct. Could be caught by unit tests though :-P
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners



_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Rein Henrichs
You can't do this at the type level in Haskell.

On Mon, Jun 22, 2015 at 7:00 AM Matt Williams <[hidden email]> wrote:
OK, I think this is clearly well beyond my level!

Will insert some manual checking.

Thanks,
Matt

On 22 June 2015 at 14:51, emacstheviking <[hidden email]> wrote:
It *could* be done and might already have been done... I seem to recall a few months back somebody asked for a similar feature using one of the vector libraries, to limit one of the input vectors to a fixed length?

You'd have to dig through the list archives though...

On 22 June 2015 at 12:36, Imants Cekusins <[hidden email]> wrote:
> But this is checking the values in the implementation, not a type level
build time guarantee, isn't it?

yep, correct. Could be caught by unit tests though :-P
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Petr Vápenka
Maybe not exactly what you need but this was for me a kind of eye-opener with regard to type system:


On Mon, Jun 22, 2015 at 9:09 PM, Rein Henrichs <[hidden email]> wrote:
You can't do this at the type level in Haskell.

On Mon, Jun 22, 2015 at 7:00 AM Matt Williams <[hidden email]> wrote:
OK, I think this is clearly well beyond my level!

Will insert some manual checking.

Thanks,
Matt

On 22 June 2015 at 14:51, emacstheviking <[hidden email]> wrote:
It *could* be done and might already have been done... I seem to recall a few months back somebody asked for a similar feature using one of the vector libraries, to limit one of the input vectors to a fixed length?

You'd have to dig through the list archives though...

On 22 June 2015 at 12:36, Imants Cekusins <[hidden email]> wrote:
> But this is checking the values in the implementation, not a type level
build time guarantee, isn't it?

yep, correct. Could be caught by unit tests though :-P
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners



_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Kostiantyn Rybnikov
In reply to this post by Matt Williams-2
Hi Matt. I don't know how bad is this, but here's what I came up with.

In order to be able to ask types to make sure something about values (their equality), you might want to create a type, which contains a value in its type-parameter, and then ask that types are equal if you want some equality property in datatype. Here's an example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

module Main where

import GHC.TypeLits

newtype TypeValInt (n::Nat) = TypeValInt Int
    deriving (Show)

one :: TypeValInt 1
one = TypeValInt 1

two :: TypeValInt 2
two = TypeValInt 2

data MyP a b = MyP (TypeValInt a, TypeValInt b) (TypeValInt b, TypeValInt a)
    deriving (Show)

main :: IO ()
main = do
    putStrLn "Hello!"
    print (MyP (one, two) (two, one))
    -- | this will error:
    -- print (MyP (one, two) (one, one))
    print (MyPGen (one, two) (two, one))
    -- | this will error:
    -- print (MyPGen (one, two) (one, one))

class TypeVal (g :: a -> *)
instance TypeVal TypeValInt

data MyPGen a b = forall g. (TypeVal g, Show (g a), Show (g b))
               => MyPGen (g a, g b) (g b, g a)
deriving instance Show (MyPGen a b)


On Mon, Jun 22, 2015 at 1:29 PM, Matt Williams <[hidden email]> wrote:

Dear All,

I wonder if/ how this is possible?

I have a constructor which takes 2 pairs of type t).

However, I want to ensure that the pairs are matched:

MyP = MyP (t, t) (t, t)

But where the first pair contains the same elements as the second, but reversed in order.

Any help much appreciated.

BW,
Matt


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners



_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Imants Cekusins
On 23 June 2015 at 14:54, Kostiantyn Rybnikov <[hidden email]> wrote:
> Hi Matt. I don't know how bad is this, but here's what I came up with.
...

this modified for IO version accepts any input, including that which
should have caused error:

or did I do something wrong?


{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

module PairsMatchedKR where

import GHC.TypeLits

data TypeValInt (n::Nat) = TypeValInt Int
    deriving (Show)

one :: TypeValInt 1
one = TypeValInt 1

two :: TypeValInt 2
two = TypeValInt 2

data MyP a b = MyP (TypeValInt a, TypeValInt b) (TypeValInt b, TypeValInt a)
    deriving (Show)

main :: IO ()
main = do
    putStrLn "Hello!"
    x1 <- getLine
    x2 <- getLine
    x3 <- getLine
    x4 <- getLine

    print (MyP (tvi x1, tvi x2) (tvi x3, tvi x4))

class TypeVal (g :: a -> *)
instance TypeVal TypeValInt

data MyPGen a b = forall g. (TypeVal g, Show (g a), Show (g b))
               => MyPGen (g a, g b) (g b, g a)
deriving instance Show (MyPGen a b)


tvi:: String -> TypeValInt (n::Nat)
tvi = TypeValInt . read
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Kostiantyn Rybnikov
Imants,

You are right. The problem is not in IO here, it's that if you have access to data-constructor, you can do things like:

six :: TypeValInt 6
six = TypeValInt 5

Initially, I was making an assumption that you won't be using a data-constructor. After thinking about it a bit, I should note that my code isn't much different from just using a "smart constructor" approach, e.g. hiding a real MyP constructor, and instead providing a function:

mkMyP (a, b) = MyP (a, b) (b, a)

and exporting only this function. This would make sure all your users only create a valid set of data.


On Tue, Jun 23, 2015 at 5:05 PM, Imants Cekusins <[hidden email]> wrote:
On 23 June 2015 at 14:54, Kostiantyn Rybnikov <[hidden email]> wrote:
> Hi Matt. I don't know how bad is this, but here's what I came up with.
...

this modified for IO version accepts any input, including that which
should have caused error:

or did I do something wrong?


{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

module PairsMatchedKR where

import GHC.TypeLits

data TypeValInt (n::Nat) = TypeValInt Int
    deriving (Show)

one :: TypeValInt 1
one = TypeValInt 1

two :: TypeValInt 2
two = TypeValInt 2

data MyP a b = MyP (TypeValInt a, TypeValInt b) (TypeValInt b, TypeValInt a)
    deriving (Show)

main :: IO ()
main = do
    putStrLn "Hello!"
    x1 <- getLine
    x2 <- getLine
    x3 <- getLine
    x4 <- getLine

    print (MyP (tvi x1, tvi x2) (tvi x3, tvi x4))

class TypeVal (g :: a -> *)
instance TypeVal TypeValInt

data MyPGen a b = forall g. (TypeVal g, Show (g a), Show (g b))
               => MyPGen (g a, g b) (g b, g a)
deriving instance Show (MyPGen a b)


tvi:: String -> TypeValInt (n::Nat)
tvi = TypeValInt . read
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Matt Williams-2

Dear All,

This has reminded me that perhaps there is an easier way.

I have a Map, whose elements are indexed by a subset of their structure.

I.e. if we have MyType = MyType I T T O E

Where I T O and E are types defined elsewhere.

The Map the indexes elements of type MyType by a pair, (T, T).

I want to be able to index by a pair, independent of order. I had thought about indexing by a pair of pairs, where the elemtns could be the same but reversed.

However, the alternative might be to index by a pair, but define that pair as a type, and alter its Eq => definition:

MyPair = (T, T)
where (t, t') == (t', t) -- I know this syntax is wrong

I could then use that as the index to the Map.

Does that approach make some sense?

Thanks,
Matt


On Tue, 23 Jun 2015 15:33 Kostiantyn Rybnikov <[hidden email]> wrote:
Imants,

You are right. The problem is not in IO here, it's that if you have access to data-constructor, you can do things like:

six :: TypeValInt 6
six = TypeValInt 5

Initially, I was making an assumption that you won't be using a data-constructor. After thinking about it a bit, I should note that my code isn't much different from just using a "smart constructor" approach, e.g. hiding a real MyP constructor, and instead providing a function:

mkMyP (a, b) = MyP (a, b) (b, a)

and exporting only this function. This would make sure all your users only create a valid set of data.


On Tue, Jun 23, 2015 at 5:05 PM, Imants Cekusins <[hidden email]> wrote:
On 23 June 2015 at 14:54, Kostiantyn Rybnikov <[hidden email]> wrote:
> Hi Matt. I don't know how bad is this, but here's what I came up with.
...

this modified for IO version accepts any input, including that which
should have caused error:

or did I do something wrong?


{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

module PairsMatchedKR where

import GHC.TypeLits

data TypeValInt (n::Nat) = TypeValInt Int
    deriving (Show)

one :: TypeValInt 1
one = TypeValInt 1

two :: TypeValInt 2
two = TypeValInt 2

data MyP a b = MyP (TypeValInt a, TypeValInt b) (TypeValInt b, TypeValInt a)
    deriving (Show)

main :: IO ()
main = do
    putStrLn "Hello!"
    x1 <- getLine
    x2 <- getLine
    x3 <- getLine
    x4 <- getLine

    print (MyP (tvi x1, tvi x2) (tvi x3, tvi x4))

class TypeVal (g :: a -> *)
instance TypeVal TypeValInt

data MyPGen a b = forall g. (TypeVal g, Show (g a), Show (g b))
               => MyPGen (g a, g b) (g b, g a)
deriving instance Show (MyPGen a b)


tvi:: String -> TypeValInt (n::Nat)
tvi = TypeValInt . read
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Imants Cekusins
> alter its Eq => definition

module MatchTuple (MyP) where

data MyP t = MyP(t,t) deriving Show
instance Eq t => Eq (MyP t)  where
   (==) = match


match::Eq t =>  MyP t-> MyP t -> Bool
match (MyP(x1,x2)) (MyP(x3,x4))
   | x1 == x3 &&  x2 == x4 = True
   | x1 == x4 &&  x2 == x3 = True
   | otherwise = False


?
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Rein Henrichs
FYI, Data.Map uses an Ord instance for keys, not an Eq instance.

On Tue, Jun 23, 2015 at 1:15 PM Imants Cekusins <[hidden email]> wrote:
> alter its Eq => definition

module MatchTuple (MyP) where

data MyP t = MyP(t,t) deriving Show
instance Eq t => Eq (MyP t)  where
   (==) = match


match::Eq t =>  MyP t-> MyP t -> Bool
match (MyP(x1,x2)) (MyP(x3,x4))
   | x1 == x3 &&  x2 == x4 = True
   | x1 == x4 &&  x2 == x3 = True
   | otherwise = False


?
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Structural restrictions in type constructor

Imants Cekusins
> Data.Map uses an Ord instance for keys, not an Eq instance.

Cheers Rein

Ord instance needs to implement compare then also
http://hackage.haskell.org/package/base-4.8.0.0/docs/Data-Ord.html
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners