[Haskell-cafe] Associated types, kind constraints & typelits

Nathan Howell nathan.d.howell at gmail.com
Tue Jan 7 16:54:33 UTC 2014


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 <hesselink at gmail.com> wrote:

> 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 <nathan.d.howell at gmail.com>
> 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 <nicolas at incubaid.com>
> > 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
> >> Haskell-Cafe at haskell.org
> >> http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
> >
> >
> > _______________________________________________
> > 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/20140107/65121483/attachment.html>


More information about the Haskell-Cafe mailing list