
Hello suppose that I have a bunch of type like this data Unchecked data Hdf5 data Cbf data A t > A String The A thing come from a database as A Unchecked now if I read the String and it ends with .h5, I have a A Hdf5 type and If the string end with .cbf, I have a A Cbf. So I would like a function which allow to return a A Hdf5 or a A Cbf depending on the String content. check :: A Unchecked -> A ??? check = ??? Is it possible to do this ? Thanks Frederic PS: At the end I will have more tha one tag.

Hello Frederic, On Tue, Oct 02, 2018 at 04:48:09PM +0000, PICCA Frederic-Emmanuel wrote:
So I would like a function which allow to return a A Hdf5 or a A Cbf depending on the String content.
check :: A Unchecked -> A ??? check = ???
Is it possible to do this ?
I believe you can do this with GADTs [1] [1] https://en.wikibooks.org/wiki/Haskell/GADT

Unfortunately I do not know the fancy Haskell type-level stuff, but if I was looking at this same problem, I'd think you need a sum type: data Unchecked = Unchecked String data Checked = Hd5 String | Cbf String check :: Unchecked -> Checked There is likely a better concept than "Checked" in your domain. I do not know what those things represent, but I would use that *ubiquitous language* instead - i.e., data Image ... instead of Checked. On Tue, Oct 2, 2018 at 12:05 PM PICCA Frederic-Emmanuel < frederic-emmanuel.picca@synchrotron-soleil.fr> wrote:
I believe you can do this with GADTs [1]
I can create different constructors for the different types. but how can I create a function which return different type ?
Fred _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
-- Steven Leiva 305.528.6038 leiva.steven@gmail.com http://www.linkedin.com/in/stevenleiva

You need to have some sort of either type. check :: A Unchecked -> Either (A Hdf5) (A Cbf) But you'll have to deal with the fact that it could be either of those things throughout the rest of your program, somehow. Another way would be to have data CheckedType = Hdf5 | Cbf check :: A Unchecked -> A CheckedType But this has the same downside. There may be some way with the singletons library, but I think that is out of the scope of the newbies list. On Tue, Oct 2, 2018 at 1:04 PM PICCA Frederic-Emmanuel < frederic-emmanuel.picca@synchrotron-soleil.fr> wrote:
I believe you can do this with GADTs [1]
I can create different constructors for the different types. but how can I create a function which return different type ?
Fred _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

On Tue, Oct 02, 2018 at 05:04:42PM +0000, PICCA Frederic-Emmanuel wrote:
I believe you can do this with GADTs [1]
I can create different constructors for the different types. but how can I create a function which return different type ?
Mhhh I tried to come up with an example (GADTs, ExistentialQuantification, etc.) and failed... This is an interesting problem and one that could interest many people; please post your question on -cafe too (with a minimal .hs, it always helps); I am curious on how they will approach the problem -F

As this problem requires type to depend on runtime value, you need singletons.
data Format = Hdf5 | Cbf
data SFormat a where -- this is called a singleton type
SHdf5 :: SFormat Hdf5
SCbf :: SFormat Cbf
data A (t::Format) = A String
data SomeA where SomeA :: SFormat f -> A f -> SomeA
check :: String -> SomeA
check "foo" = SomeA SHdf5 (A "foo")
check "bar" = SomeA SCbf (A "bar")
you can recover the type of A be pattern-matching:
someFunc :: SomeA -> A Hdf5
someFunc (SomeA SHdf5 a) = a -- a has type A Hdf5 here, equation typechecks
someFunc (SomeA SCbf a) = a -- a has type A SCbf here, this is a type error
You will need KindSignatures, DataKinds and GADTs language extensions.
With some effort you can probably add Unchecked type tag to the
picture if you don't want to use just Strings for A Unchecked.
One downside of this method is that you need to enumerate all the
possible tags twice. There is a singletons package [1] that can
automatically generate SFormat for you.
[1] http://hackage.haskell.org/package/singletons
On 03/10/2018, Francesco Ariis
On Tue, Oct 02, 2018 at 05:04:42PM +0000, PICCA Frederic-Emmanuel wrote:
I believe you can do this with GADTs [1]
I can create different constructors for the different types. but how can I create a function which return different type ?
Mhhh I tried to come up with an example (GADTs, ExistentialQuantification, etc.) and failed...
This is an interesting problem and one that could interest many people; please post your question on -cafe too (with a minimal .hs, it always helps); I am curious on how they will approach the problem
-F
_______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
-- Никита Фуфаев, +7 999 825-95-07

Hi Everyone,
I tried to come up with a solution, but it has plenty of drawbacks.
data Tag = Hdf5 | Cbf | Unchecked
data A :: Tag -> Type where
Ca :: Symbol -> A Unchecked
Ch :: A Hdf5
Cb :: A Cbf
type family Typestring (a :: A Unchecked) :: Type
type instance Typestring (Ca "hdf5") = A Hdf5
type instance Typestring (Ca "cbf") = A Cbf
data SUnchecked a where
Sh :: SUnchecked (Ca "hdf5")
Sc :: SUnchecked (Ca "cbf")
This checkValue function is useless, because you need to pass A Unchecked,
and constructor (Ca) takes Symbol rather than String, and value of type
SUnchecked a.
checkValue :: forall (a :: A Unchecked). A Unchecked -> SUnchecked a ->
Typestring a
checkValue (Ca x) Sh = Ch
checkValue (Ca x) Sc = Cb
When I tried to run the above code
*Main> :t checkValue (Ca (someSymbolVal "hdf5"))
<interactive>:1:17: error:
• Couldn't match expected type ‘Symbol’
with actual type ‘GHC.TypeLits.SomeSymbol’
• In the first argument of ‘Ca’, namely ‘(someSymbolVal "hdf5")’
In the first argument of ‘checkValue’, namely
‘(Ca (someSymbolVal "hdf5"))’
In the expression: checkValue (Ca (someSymbolVal "hdf5"))
What I really want is something like this, but the problem is I can't do
pattern matching on symbols, and if I change the data type to String from
Symbol then it won't compile .
Could some one point me how to solve this problem?
checkValue :: forall (a :: A Unchecked). SUnchecked a => A Unchecked ->
Typestring a
checkValue (Ca "hdf5") = Ch
checkValue (Ca "cbf") = Cb
Best regards,
Mukesh
On Thu, Oct 4, 2018 at 11:11 PM Francesco Ariis
Hello Nikita,
On Thu, Oct 04, 2018 at 02:50:09AM +0300, Никита Фуфаев wrote:
As this problem requires type to depend on runtime value, you need singletons.
Many thanks for showing us the way, very elegant solution. _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

Hello, So I end-up for now with two singletons for my SomeDataCollection So I red the Datacollection from an xml file (col) then I create the SomeDataCollection type depending on a bunch of values found in the Datacollection. like this. return $ if "ref-" `isPrefixOf` imagePrefix col then case imageSuffix col of (Just "cbf") -> SomeDataCollection SCaracterization SCbf (coerce col) (Just "h5") -> SomeDataCollection SCaracterization SHdf5 (coerce col) (Just _) -> SomeDataCollection SCaracterization SCbf (coerce col) Nothing -> SomeDataCollection SCaracterization SCbf (coerce col) else case imageSuffix col of (Just "cbf") -> SomeDataCollection SCollect SCbf (coerce col) (Just "h5") -> SomeDataCollection SCollect SHdf5 (coerce col) (Just _) -> SomeDataCollection SCollect SCbf (coerce col) Nothing -> SomeDataCollection SCollect SCbf (coerce col) Now I would like to do something like let t = if "ref-" `isPrefixOf` imagePrefix col then SCaracterization else SCollect and then return SomeDatacollection t f (coerce col) But If I try to do this I have an error like this src/ISPyB/Soap.hs:119:37-44: error: • Couldn't match type ‘'Collect’ with ‘'Caracterization’ Expected type: SCollectType 'Caracterization Actual type: SCollectType 'Collect • In the expression: SCollect In the expression: if "ref-" `isPrefixOf` imagePrefix col then SCaracterization else SCollect In an equation for ‘t’: t = if "ref-" `isPrefixOf` imagePrefix col then SCaracterization else SCollect how can I fix this and make the code better to read. thanks Fred

return (if "ref-" `isPrefixOf` imagePrefix col
then
cont SCaracterization
else
cont SCollect)
where
cont :: forall coc. SCaracterizationOrCollect coc -> SomeDataCollection
cont sing = case imageSuffix col of
(Just "cbf") -> SomeDataCollection sing SCbf (coerce col)
(Just "h5") -> SomeDataCollection sing SHdf5 (coerce col)
(Just _) -> SomeDataCollection sing SCbf (coerce col)
Nothing -> SomeDataCollection sing SCbf (coerce col)
You could also get rid of SomeDataCollection in a similar way:
data DataCollection a b = DataCollection (SCaracterizationOrCollect a)
(SSuffix b) String
parseFileName :: forall c. String -> (forall a b. DataCollection a b -> c) -> c
parseFileName col cont = (if "ref-" `isPrefixOf` imagePrefix col
then
cont2 SCaracterization
else
cont2 SCollect)
where cont2 :: forall coc. SCaracterizationOrCollect coc -> c
cont2 sing = case imageSuffix col of
(Just "cbf") -> cont $ DataCollection sing SCbf (coerce col)
(Just "h5") -> cont $ DataCollection sing SHdf5 (coerce col)
(Just _) -> cont $ DataCollection sing SCbf (coerce col)
Nothing -> cont $ DataCollection sing SCbf (coerce col)
In general, when you want to type some expression that can be of
different types depending on values, you can turn it into a function
that takes polymorphic continuation as an argument.
If you plan to have many tags on DataCollection and many functions
that return DataCollections of different types where some tags depend
on argument values and some tags are staticlly known, this style is
probably easier.
If you are willing to use singletons package, there is another way to do this:
{-# Language TemplateHaskell, KindSignatures, TypeFamilies, DataKinds,
ScopedTypeVariables #-}
import Data.Coerce
import Data.Singletons.TH
import Data.List
$(singletons [d|
data Suffix = Cbf | Hdf5
data CaracterizationOrCollect = Caracterization | Collect
|])
data SomeDataCollection where
SomeDataCollection :: SCaracterizationOrCollect a -> SSuffix b ->
DataCollection a b -> SomeDataCollection
newtype DataCollection (a::CaracterizationOrCollect) (b::Suffix) = DC String
someFunc :: String -> IO SomeDataCollection
someFunc col = return $ withSomeSing (if "ref-" `isPrefixOf` imagePrefix col
then
Caracterization
else
Collect)
(\sing -> case imageSuffix col of
(Just "cbf") ->
SomeDataCollection sing SCbf (coerce col)
(Just "h5") ->
SomeDataCollection sing SHdf5 (coerce col)
(Just _) ->
SomeDataCollection sing SCbf (coerce col)
Nothing -> SomeDataCollection
sing SCbf (coerce col))
Hopefully, when the hyped DependentTypes extension lands, this will
all be authomated and we won't need to explicitly use a single
singleton anymore.
On 11/10/2018, PICCA Frederic-Emmanuel
Hello, So I end-up for now with two singletons for my SomeDataCollection
So I red the Datacollection from an xml file (col) then I create the SomeDataCollection type depending on a bunch of values found in the Datacollection. like this.
return $ if "ref-" `isPrefixOf` imagePrefix col then case imageSuffix col of (Just "cbf") -> SomeDataCollection SCaracterization SCbf (coerce col) (Just "h5") -> SomeDataCollection SCaracterization SHdf5 (coerce col) (Just _) -> SomeDataCollection SCaracterization SCbf (coerce col) Nothing -> SomeDataCollection SCaracterization SCbf (coerce col) else case imageSuffix col of (Just "cbf") -> SomeDataCollection SCollect SCbf (coerce col) (Just "h5") -> SomeDataCollection SCollect SHdf5 (coerce col) (Just _) -> SomeDataCollection SCollect SCbf (coerce col) Nothing -> SomeDataCollection SCollect SCbf (coerce col)
Now I would like to do something like
let t = if "ref-" `isPrefixOf` imagePrefix col then SCaracterization else SCollect
and then
return SomeDatacollection t f (coerce col)
But If I try to do this I have an error like this
src/ISPyB/Soap.hs:119:37-44: error: • Couldn't match type ‘'Collect’ with ‘'Caracterization’ Expected type: SCollectType 'Caracterization Actual type: SCollectType 'Collect • In the expression: SCollect In the expression: if "ref-" `isPrefixOf` imagePrefix col then SCaracterization else SCollect In an equation for ‘t’: t = if "ref-" `isPrefixOf` imagePrefix col then SCaracterization else SCollect
how can I fix this and make the code better to read.
thanks
Fred _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
-- Nikita Fufaev, +7 999 825-95-07

I endup with this solution, whcih is for me quite elegant. Maybe this could be generalize with the singleton package. mkSomeDataCollection :: DataCollection a b -> SomeDataCollection mkSomeDataCollection c = withSCollectType $ \s -> withSCollectSourceFormat $ \f -> SomeDataCollection s f (coerce c) where withSCollectType :: (forall c. SCollectType c -> SomeDataCollection) -> SomeDataCollection withSCollectType cont = if "ref-" `isPrefixOf` imagePrefix c then cont SCaracterization else cont SCollect withSCollectSourceFormat :: (forall c .SCollectSourceFormat c -> SomeDataCollection) -> SomeDataCollection withSCollectSourceFormat cont = case imageSuffix c of (Just "cbf") -> cont SCbf (Just "h5") -> cont SHdf5 (Just _) -> cont SCbf Nothing -> cont SCbf I can not use singleton since I decided to stick to Debian stable/unstable Cheers and thanks a lot for the help. Frederic

Nervertheless, what is the advantage of this Singleton things vs a TypeClass with an instance by type ?

I'm not sure what you mean by TypeClass with an instance by type
method, can you elaborate on that?
BTW i'm sorry for poor formatting in my messages, i hope my code
samples are understandable despite the fact that there are line breaks
in them where there shouldn't be.
On 12/10/2018, PICCA Frederic-Emmanuel
Nervertheless, what is the advantage of this Singleton things vs a TypeClass with an instance by type ? _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
-- Nikita Fufaev, +7 999 825-95-07

Hi Fredric, below are two ways to solve it, first with GADTs, the other with type classes. But I think in both cases you need to define the specific handling of the types in multiple places. With GADT's you need to add yet another constructor for yet another `t`. With type classes you need to specify the type in-line at the place you branch off, not sure how elegant that is. The singleton based approach is perhaps better than both of the below if your set of types is closed, since you only keep the string in one data constructor (in the `A "here"`), while with a GADT you have it nested in one of the AHdf5 or ACbf. On the other hand singletons need some extensions to be turned. Hope it helps, code follows: data A t = A String data Unchecked data Hdf5 data Cbf -- * A with GADT data A' where AHdf5 :: A Hdf5 -> A' ACbf :: A Cbf -> A' AUnchecked :: A Unchecked -> A' check :: A Unchecked -> A' check a = case a of A str | suffix ".h5" -> AHdf5 (A str) | suffix ".cdf" -> ACbf (A str) | otherwise -> AUnchecked (A str) where suffix suf = suf `isSuffixOf` str -- * Type classes type SomethnigCommon = () class Continue a where go :: A a -> SomethnigCommon instance Continue Hdf5 where go (A hdf5) = undefined -- implementation for hdf5 here instance Continue Cbf where go (A cbf) = undefined -- implementation for cbf here instance Continue Unchecked where go (A unchecked) = undefined -- implementation for unchecked here check' :: A Unchecked -> SomethnigCommon check' a = case a of A str | suffix ".h5" -> go (A str :: A Hdf5) | suffix ".cdf" -> go (A str :: A Cbf) | otherwise -> go (A str :: A Unchecked) where suffix suf = suf `isSuffixOf` str On Tue, Oct 2, 2018 at 6:48 PM PICCA Frederic-Emmanuel < frederic-emmanuel.picca@synchrotron-soleil.fr> wrote:
Hello
suppose that I have a bunch of type like this
data Unchecked data Hdf5 data Cbf
data A t > A String
The A thing come from a database as A Unchecked
now if I read the String and it ends with .h5, I have a A Hdf5 type and If the string end with .cbf, I have a A Cbf.
So I would like a function which allow to return a A Hdf5 or a A Cbf depending on the String content.
check :: A Unchecked -> A ??? check = ???
Is it possible to do this ?
Thanks
Frederic
PS: At the end I will have more tha one tag. _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
-- Markus Läll
participants (8)
-
David McBride
-
Francesco Ariis
-
Markus Läll
-
mukesh tiwari
-
Nikita Fufaev
-
PICCA Frederic-Emmanuel
-
Steven Leiva
-
Никита Фуфаев