All,
While toying with typelits I wanted to get the following to work, but failed to. Is it intended not to work at all, should I change something to get it to work, or is this something which needs some GHC support? Note I obviously tried to add the constraint mentioned in the compiler error, but failed to: I seem to add too many type arguments to SingI, which somewhat puzzles me. Thanks, Nicolas {-# LANGUAGE TypeFamilies, DataKinds #-} module Main where import GHC.TypeLits class C a where type T a :: Nat data D = D instance C D where type T D = 10 {- This is not allowed, as intended: data E = E instance C E where type T E = Int -} -- This works: tOfD :: D -> Integer tOfD D = fromSing $ (sing :: Sing (T D)) {- This doesn't work: - Could not deduce (SingI Nat (T a1)) arising from a use of `sing' - from the context (C a) tOf :: C a => a -> Integer tOf _ = fromSing $ (sing :: Sing (T a)) -} main :: IO () main = return () _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
This requires -XScopedTypeVariables and some constraints:
tOf :: forall a . (SingI (T a), C a) => a -> Integer tOf _ = fromSing $ (sing :: Sing (T a)) On Mon, Jan 6, 2014 at 9:06 AM, Nicolas Trangez <[hidden email]> wrote: All, _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Mon, 2014-01-06 at 09:15 -0800, Nathan Howell wrote:
> This requires -XScopedTypeVariables and some constraints: > > tOf :: forall a . (SingI (T a), C a) => a -> Integer > tOf _ = fromSing $ (sing :: Sing (T a)) Wonderful, thanks. I tried using ScopedTypeVariables, but "SingI Nat (T a)" didn't work out, although the compiler error hinted in that direction. Thanks, Nicolas _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Nathan Howell-2
Small additions: the 'Nat' in the original argument is the kind
argument to the class. It seems to be a bug that GHC provided this in the error, and the latest HEAD doesn't seem to do so anymore. Also, in the latest HEAD, I think you need to use the singletons library, as all the singletons stuff is gone from base. My working code: {-# LANGUAGE TypeFamilies , DataKinds , FlexibleContexts , ScopedTypeVariables #-} module Main where import GHC.TypeLits import Data.Singletons class C a where type T a :: Nat data D = D instance C D where type T D = 10 {- This is not allowed, as intended: data E = E instance C E where type T E = Int -} -- This works: tOfD :: D -> Integer tOfD D = fromSing $ (sing :: Sing (T D)) tOf :: forall a. (KnownNat (T a), C a) => a -> Integer tOf _ = fromSing $ (sing :: Sing (T a)) main :: IO () main = return () Erik On Mon, Jan 6, 2014 at 6:15 PM, Nathan Howell <[hidden email]> wrote: > This requires -XScopedTypeVariables and some constraints: > > tOf :: forall a . (SingI (T a), C a) => a -> Integer > tOf _ = fromSing $ (sing :: Sing (T a)) > > > On Mon, Jan 6, 2014 at 9:06 AM, Nicolas Trangez <[hidden email]> > wrote: >> >> All, >> >> While toying with typelits I wanted to get the following to work, but >> failed to. Is it intended not to work at all, should I change something >> to get it to work, or is this something which needs some GHC support? >> >> Note I obviously tried to add the constraint mentioned in the compiler >> error, but failed to: I seem to add too many type arguments to SingI, >> which somewhat puzzles me. >> >> Thanks, >> >> Nicolas >> >> {-# LANGUAGE TypeFamilies, >> DataKinds #-} >> module Main where >> >> import GHC.TypeLits >> >> class C a where >> type T a :: Nat >> >> data D = D >> instance C D where >> type T D = 10 >> >> {- This is not allowed, as intended: >> >> data E = E >> instance C E where >> type T E = Int >> -} >> >> -- This works: >> tOfD :: D -> Integer >> tOfD D = fromSing $ (sing :: Sing (T D)) >> >> {- This doesn't work: >> - Could not deduce (SingI Nat (T a1)) arising from a use of `sing' >> - from the context (C a) >> >> tOf :: C a => a -> Integer >> tOf _ = fromSing $ (sing :: Sing (T a)) >> -} >> >> main :: IO () >> main = return () >> >> _______________________________________________ >> Haskell-Cafe mailing list >> [hidden email] >> http://www.haskell.org/mailman/listinfo/haskell-cafe > > > > _______________________________________________ > Haskell-Cafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe > Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
natVal accepts any type witness now, not just sing. One such type in base is the polykinded Data.Proxy.Proxy, e.g. `natVal (Proxy :: Proxy 0`. For types of kind * you can use almost anything, including an empty list.
On Mon, Jan 6, 2014 at 9:27 AM, Erik Hesselink <[hidden email]> wrote: Small additions: the 'Nat' in the original argument is the kind _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |