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

[Bardur Arantsson]

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,