Structural restrictions in type constructor
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
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
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"
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
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 <imantc@gmail.com> 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
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 <objitsu@gmail.com> 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 <imantc@gmail.com> 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
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 <objitsu@gmail.com> 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 <imantc@gmail.com> 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
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 <rein.henrichs@gmail.com> 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 <objitsu@gmail.com> 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 <imantc@gmail.com> 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
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 <matt.williams45.mw@gmail.com
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
On 23 June 2015 at 14:54, Kostiantyn Rybnikov <k-bx@k-bx.com> 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
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 <imantc@gmail.com> wrote:
On 23 June 2015 at 14:54, Kostiantyn Rybnikov <k-bx@k-bx.com> 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
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 <k-bx@k-bx.com> 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 <imantc@gmail.com> wrote:
On 23 June 2015 at 14:54, Kostiantyn Rybnikov <k-bx@k-bx.com> 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
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 ?
FYI, Data.Map uses an Ord instance for keys, not an Eq instance. On Tue, Jun 23, 2015 at 1:15 PM Imants Cekusins <imantc@gmail.com> 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
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
participants (7)
-
emacstheviking -
Imants Cekusins -
Kostiantyn Rybnikov -
Martin Vlk -
Matt Williams -
Petr Vápenka -
Rein Henrichs