[Haskell-beginners] 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 <fa-ml at ariis.it> 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
> Beginners at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20181006/ed646e8d/attachment.html>