Opened 2 months ago

Last modified 2 months ago

#8778 new feature request

Typeable TypeNats

Reported by: dmcclean Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.1-rc1
Keywords: Cc: bjorn.buckwalter@…, iavor.diatchki@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets: 4385


It would be useful (the case I have at hand is for some scenarios involving checking of physical dimensions) to be able to combine the Data.Dynamic story with the GHC.TypeLits? story.

A Typeable instance for every Nat is the sticking point.

(I do not know if this is even theoretically possible.)

Attachments (1)

Test8778.hs (246 bytes) - added by dmcclean 2 months ago.
Test case

Download all attachments as: .zip

Change History (7)

comment:1 Changed 2 months ago by BjornBuckwalter

  • Cc bjorn.buckwalter@… added

comment:2 Changed 2 months ago by carter

@dmcclean could you please explain what you mean? Make up some pseudo code please!

Are you thinking about type level existentials?

comment:3 Changed 2 months ago by thoughtpolice

  • Version 7.8.1-rc1 deleted

This isn't going to happen in time for 7.8.1.

Changed 2 months ago by dmcclean

Test case

comment:4 Changed 2 months ago by dmcclean

Sorry about that, thoughtpolice, I was thinking the field was for where I saw it.

Example (also attached, but here for discussion):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE AutoDeriveTypeable #-}

module Test8778 where

import GHC.TypeLits
import Data.Dynamic

data Phantom (n :: Nat) = Phantom

desirable = toDyn (Phantom :: Phantom 3)

Results in:

    No instance for (Typeable 3) arising from a use of `toDyn'
    In the expression: toDyn (Phantom :: Phantom 3)
    In an equation for `desirable':
        desirable = toDyn (Phantom :: Phantom 3)
Failed, modules loaded: none.

This is unfortunate because it means that you can't use Data.Dynamic with any types that have phantom Nat parameters. Up a couple of levels in the abstraction hierarchy, this makes it difficult to build a user interface that works well with displaying signals and taking input of arbitrary dimensional types (lengths, velocities, currents, and the like).

comment:5 Changed 2 months ago by thoughtpolice

  • Version set to 7.8.1-rc1

Actually I was sort of reclassifying the tickets and that was my mistake to remove the version :) I've changed it back. And thank you for the example!

comment:6 Changed 2 months ago by dreixel

  • Cc iavor.diatchki@… added

Iavor has looked into this, so he might have some status update...

Note: See TracTickets for help on using tickets.