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

[James M]

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

The error I get is this:

    Couldn't match type 'k' with ''FOLDER'
      'k' is a rigid type variable bound by
          a pattern with constructor
            SomeEntry :: forall (k :: FileKind). Entry k -> SomeEntry,
          in an equation for 'convertBack'
          at cafe2.hs:24:14
    Expected type: Entry 'FOLDER
      Actual type: Entry k
    Relevant bindings include x :: Entry k (bound at cafe2.hs:24:24)
    In the first argument of 'Right', namely 'x'
    In the expression: Right x

James


On Wed, Nov 12, 2014 at 11:29 PM, Bardur Arantsson <spam at scientician.net>
wrote:

> On 2014-11-13 08:10, James M wrote:
> > I didn't explain Frank's case, only the one I constructed.
> >
> > convertBack :: SomeEntry -> Either (FsEntry FILE) (FsEntry FOLDER)
> >
> > For this function to work, we would need some way to inspect the type as
> a
> > value, and this can only generally be done with dependent types.
> >
> > convertBack :: SomeEntry -> FsEntry k
> >
> > This case is technically possible to do statically, but not very useful
> > because we have no idea what the actual type is. Therefore, we could only
> > use it on things that work for all FsEntry and not just a subset.
> >
> > We could ask for what 'k' is in the type system and perform the necessary
> > computation in the type system. However, this is complicated, and Haskell
> > currently only has very limited support for moving between values and
> > types. You can look at GHC.TypeLits for an example of this.
>
> Maybe I'm missing something, but wouldn't adding a Typeable constraint
> on the existential give you the option of casting back? AFAICT that
> should be sufficient since the FileKind is closed and you can thus just
> attempt both conversions and see which one succeeds.
>
> Regards,
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141112/ed7aea07/attachment.html>