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

13 Nov 2014

      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  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 
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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe