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

[James M]

To explain, you should think of

forall (k :: FileKind) . Entry k

as being different than

Entry 'FOLDER
Entry 'FILE

The difference being that anything that is 'k' must be able to satisfy all
FileKind not just one of them.

James

On Wed, Nov 12, 2014 at 11:47 PM, James M <jmartin at eecs.berkeley.edu> wrote:

> 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/424e4785/attachment-0001.html>