Re: [Haskell-beginners] Type depending on value

12 May 2016

      ...
{-# 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
 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?

Re: [Haskell-beginners] Type depending on value

Dmitriy Matrosov