Nicolas Trangez | 6 Jan 18:06 2014

Associated types, kind constraints & typelits

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
(Continue reading)

Nathan Howell | 6 Jan 18:15 2014
Picon

Re: Associated types, kind constraints & typelits

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
Nicolas Trangez | 6 Jan 18:21 2014

Re: Associated types, kind constraints & typelits

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
Erik Hesselink | 6 Jan 18:27 2014
Picon

Re: Associated types, kind constraints & typelits

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
>
Nathan Howell | 7 Jan 17:54 2014
Picon

Re: Associated types, kind constraints & typelits

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
>

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane