[Haskell-cafe] Representing record subtypes, sort of.

[James M]

Interesting. I wasn't aware that you could pattern match on something with
different types.

This would make GADTs more useful than the ExistentialTypes extension in
cases where you don't need the extensibility.

James

On Thu, Nov 13, 2014 at 1:11 AM, Frank Staals <frank at fstaals.net> wrote:

> James M <jmartin at eecs.berkeley.edu> writes:
>
> > This is easily testable.
> >
> > deriving instance Typeable Entry
> > deriving instance Typeable FileKind
> > deriving instance Typeable 'FOLDER
> > deriving instance Typeable 'FILE
> >
> > convertBack :: SomeEntry -> Either (Entry FILE) (Entry FOLDER)
> > convertBack (SomeEntry x)
> >     | typeOf x == typeOf (Folder "" "") = Right x
> >     | otherwise = Left x
>
>
> If the goal is just to write the `convertBack' function with the type
> signature above you don't need Typeable. If you enable the GADT
> extension you can just pattern match on the Entry that is stored in the
> SomeEntry, even though they have different types: i.e.
>
> convertBack :: SomeEntry -> Either (Entry FILE) (Entry FOLDER)
> convertBack (SomeEntry f@(File _ _ _)) = Left f
>                                          -- By pattern matching on f we
>                                          -- can convince the compiler
>                                          -- that f  is of type Entry FILE
> convertBack (SomeEntry d@(Folder _ _)) = Right d
>
> Similarly we can write a function
>
> convertAsFile :: SomeEntry -> Entry FILE
> convertAsFile (SomeEntry f@(File _ _ _)) = f
> convertAsFile (SomeEntry d) = error "We cannot convert from a Entry FOLDER"
>
> however there is no way of making that function total (i.e. in the
> second case there is no proper way of constructing an Entry FILE from an
> Entry FOLDER)
>
> Because you can (locally) recover the type by pattern matching on a GADT
> I prefer to use GADTs to model existential types rather than using the
> ExistentialTypes extension.
>
> --
>
> - Frank
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141113/a65cd5e0/attachment.html>