Structural restrictions in type constructor

newer
ghc-mod and cabal "could not find...

Matt Williams

22 Jun 2015 22 Jun '15

6:29 a.m.

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

Attachments:

attachment.html (text/html — 442 bytes)

Show replies by date

Martin Vlk

22 Jun 22 Jun

6:49 a.m.

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 Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Imants Cekusins

7:29 a.m.

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"

Martin Vlk

7:34 a.m.

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 Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Imants Cekusins

7:36 a.m.

...

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

emacstheviking

9:51 a.m.

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 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 Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Matt Williams

10 a.m.

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 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 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 Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Rein Henrichs

3:09 p.m.

You can't do this at the type level in Haskell. On Mon, Jun 22, 2015 at 7:00 AM Matt Williams 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 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 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 Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Petr Vápenka

3:18 p.m.

Maybe not exactly what you need but this was for me a kind of eye-opener with regard to type system: https://github.com/leonidas/codeblog/blob/master/2013/2013-02-19-typesafe-ti... On Mon, Jun 22, 2015 at 9:09 PM, Rein Henrichs wrote:

...

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

On Mon, Jun 22, 2015 at 7:00 AM Matt Williams < matt.williams45.mw@gmail.com> 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 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 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 Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Kostiantyn Rybnikov

23 Jun 23 Jun

8:54 a.m.

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

...

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 Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Imants Cekusins

10:05 a.m.

On 23 June 2015 at 14:54, Kostiantyn Rybnikov 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

Kostiantyn Rybnikov

10:33 a.m.

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 wrote:

...

On 23 June 2015 at 14:54, Kostiantyn Rybnikov 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 Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Matt Williams

3:21 p.m.

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 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 wrote:

...
On 23 June 2015 at 14:54, Kostiantyn Rybnikov 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 Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Imants Cekusins

4:14 p.m.

...

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 ?

Rein Henrichs

4:33 p.m.

FYI, Data.Map uses an Ord instance for keys, not an Eq instance. On Tue, Jun 23, 2015 at 1:15 PM Imants Cekusins 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 Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Imants Cekusins

4:41 p.m.

...

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

3618

Age (days ago)

3619

Last active (days ago)

List overview

Download

15 comments

7 participants

participants (7)

emacstheviking
Imants Cekusins
Kostiantyn Rybnikov
Martin Vlk
Matt Williams
Petr Vápenka
Rein Henrichs