[Haskell-beginners] 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 <fa-ml at ariis.it> 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
> Beginners at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>


-- 
Никита Фуфаев,
+7 999 825-95-07