[Haskell-beginners] Type depending on value

[Dmitriy Matrosov]

> {-# LANGUAGE DataKinds, GADTs, StandaloneDeriving, Rank2Types, PolyKinds, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables #-}
>
> data Nat = Z | S Nat
>   deriving (Show)


 On Fri, May 6, 2016 at 2:24 PM, Marcin Mrotek
<marcin.jan.mrotek at gmail.com> wrote:
 > You could define SNat as something

> newtype SNat (n :: Nat) = SNat Nat
>   deriving (Show)

 > to be on the safer side, and then define SNatClass and natVal as something
 > like:

> class SNatClass (n :: Nat) where
>   singN :: SNat n
>
> instance SNatClass Z where
>   singN = SNat Z
>
> instance SNatClass n => SNatClass (S n) where
>   singN = SNat (S n)
>     where SNat n = (singN :: SNat n)
>
> natVal :: forall n proxy. SNatClass n => proxy n -> Nat
> natVal _ = case (singN :: SNat n) of SNat n -> n

Hi.

Hm.. but such singleton definition differs from mine and i can't get it
working.  Your singleton defines function `type -> singleton`:

    *Main> singN :: SNat ('S 'Z)
    SNat (S Z)

and function `type -> Nat`:

    *Main> natVal (undefined :: SNat ('S 'Z))
    S Z

Mine singleton:

> data SNat2 :: Nat -> * where
>     SZ :: SNat2 'Z
>     SN :: SNat2 n -> SNat2 ('S n)
> deriving instance Show (SNat2 n)
>
> class SNatClass2 (a :: Nat) where
>     singN2 :: SNat2 a
>
> instance SNatClass2 'Z where
>     singN2 = SZ
> instance SNatClass2 n => SNatClass2 ('S n) where
>     singN2 = SN singN2
>
> natVal2 :: forall p n. SNatClass2 n => p n -> Nat
> natVal2 _ = case singN2 :: SNat2 n of
>               SZ    -> Z
>               SN SZ -> S Z

does this too:

    *Main> singN2 :: SNat2 ('S 'Z)
    SN SZ
    *Main> natVal2 (undefined :: SNat2 ('S 'Z))
    S Z

But mine singleton also defines function `singleton -> type`:

    *Main> :t SN SZ
    SN SZ :: SNat2 ('S 'Z)

which yours does not:

    *Main> :t SNat (S Z)
    SNat (S Z) :: SNat n

or in other words:

*Main> :t SN SZ :: SNat2 'Z
<interactive>:1:1:
    Couldn't match type ‘'S 'Z’ with ‘'Z’
    Expected type: SNat2 'Z
      Actual type: SNat2 ('S 'Z)
    In the expression: SN SZ :: SNat2 Z

but

*Main> :t SNat (S Z) :: SNat 'Z
SNat (S Z) :: SNat 'Z :: SNat 'Z

Then when i try to define recursive function on singletons, i need that
relation:

> data Vec :: * -> Nat -> * where
>     Nil  :: Vec a 'Z
>     Cons :: a -> Vec a n -> Vec a ('S n)
> deriving instance Show a => Show (Vec a n)
>
> natVec2 :: SNat2 n -> Vec Int n
> natVec2 SZ       = Nil
> natVec2 (SN n)   = Cons 1 (natVec2 n)

as i understand, here (in `natVec2`) pattern matching on value level
introduces type equalities (n ~ 'Z) or (n ~ 'S n) at type level
correspondingly.

But with your singleton it can't be done that way. I've tried to use witness
(well, i've probably used it wrong, but still..), but can't figure out how to
specify "if (n ~ 'S m), then" at type level:

> data SingInst (n :: Nat) where
>     SingInst :: SNatClass n => SingInst n
>
> singInst :: forall p n. SNatClass n => p ('S n) -> SingInst n
> singInst _ = case (singN :: SNat ('S n)) of
>                 SNat _ -> SingInst
>
> natVec :: forall p n. SNatClass2 n => p n -> Vec Int n
> natVec _ = case (singN :: SNat n) of
>               SNat Z -> Nil
>               SNat (S n) -> natVec (singInst (singN :: SNat n))

Is there a way to define `natVec` with your singleton?