Tagged types

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

Tagged types

PICCA Frederic-Emmanuel
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Tagged types

Francesco Ariis
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
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Tagged types

PICCA Frederic-Emmanuel
> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Tagged types

Steven Leiva
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 <[hidden email]> 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
[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: Tagged types

David McBride
In reply to this post by PICCA Frederic-Emmanuel
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 <[hidden email]> 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
[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: Tagged types

Francesco Ariis
In reply to this post by PICCA Frederic-Emmanuel
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Tagged types

Никита Фуфаев
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 <[hidden email]> wrote:

> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>


--
Никита Фуфаев,
+7 999 825-95-07
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Tagged types

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Tagged types

mukesh tiwari
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 <[hidden email]> wrote:
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
[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: Tagged types

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Tagged types

Никита Фуфаев
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
<[hidden email]> wrote:

> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>


--
Nikita Fufaev,
+7 999 825-95-07
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Tagged types

PICCA Frederic-Emmanuel
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
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Tagged types

PICCA Frederic-Emmanuel
Nervertheless, what is the advantage of this Singleton things vs a TypeClass with an instance by type ?
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Tagged types

Никита Фуфаев
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
<[hidden email]> wrote:
> Nervertheless, what is the advantage of this Singleton things vs a TypeClass
> with an instance by type ?
> _______________________________________________
> Beginners mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>


--
Nikita Fufaev,
+7 999 825-95-07
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners