Associated types, kind constraints & typelits

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Associated types, kind constraints & typelits

Nicolas Trangez
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
Reply | Threaded
Open this post in threaded view
|

Re: Associated types, kind constraints & typelits

Nathan Howell-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Associated types, kind constraints & typelits

Nicolas Trangez
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
Reply | Threaded
Open this post in threaded view
|

Re: Associated types, kind constraints & typelits

Erik Hesselink
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
Reply | Threaded
Open this post in threaded view
|

Re: Associated types, kind constraints & typelits

Nathan Howell-2
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
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