[Haskell-beginners] Multiplicaton of singletons

[Dmitriy Matrosov]

On Tue, Mar 15, 2016 at 1:23 PM, Dmitriy Matrosov <sgf.dma at gmail.com> wrote:

> > {-# LANGUAGE DataKinds, KindSignatures, TypeFamilies,
> UndecidableInstances #-}
>
> Hi.
>
> I've reading "Part I: Dependent Types in Haskell" by Hiromi ISHII at
> schoolofhaskell [1] and i can't understand why my multiplication for
> singletons (that was exercise) does not not work:
>
> > data Nat = Z | S Nat
> >
> > type family Plus (a :: Nat) (b :: Nat) :: Nat where
> >     Plus 'Z      b  = b
> >     Plus ('S a1) b  = 'S (Plus a1 b)
> >
> > type family Mult (a :: Nat) (b :: Nat) :: Nat where
> >     Mult 'Z      b  = 'Z
> >     Mult ('S 'Z) b  = b
> >     Mult ('S a1) b  = Plus (Mult a1 b) b
> >
> > data SNat :: Nat -> * where
> >     SZ :: SNat 'Z
> >     SN :: SNat n -> SNat ('S n)
> >
> > plusN :: SNat n -> SNat m -> SNat (Plus n m)
> > plusN SZ     y      = y
> > plusN (SN x) y      = SN (plusN x y)
> >
> > multN :: SNat n -> SNat m -> SNat (Mult n m)
> > multN SZ      y     = SZ
> > multN (SN SZ) y     = y
> > multN (SN x)  y     = plusN (multN x y) y
>
> The last line (multN) does not type-check with error:
>
> 1.lhs:31:25:
>     Could not deduce (Mult ('S n1) m ~ Plus (Mult n1 m) m)
>     from the context (n ~ 'S n1)
>       bound by a pattern with constructor
>                  SN :: forall (n :: Nat). SNat n -> SNat ('S n),
>                in an equation for ‘multN’
>       at 1.lhs:31:10-13
>     Expected type: SNat (Mult n m)
>       Actual type: SNat (Plus (Mult n1 m) m)
>     Relevant bindings include
>       y :: SNat m (bound at 1.lhs:31:17)
>       x :: SNat n1 (bound at 1.lhs:31:13)
>       multN :: SNat n -> SNat m -> SNat (Mult n m) (bound at 1.lhs:29:3)
>     In the expression: plusN (multN x y) y
>     In an equation for ‘multN’: multN (SN x) y = plusN (multN x y) y
>
> Though, when (n ~ 'S n1) i get `SNat (Mult ('S n1) m)` and by definition of
> Mult this is `SNat (Plus (Mult n1 m) m)` . On the other hand, when i check
> the
> type of expression, i get `SNat (Plus (Mult n1 m) m)` by definition of
> plusN.
> I.e. exactly the same type.
>
>
> [1]:
> https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell
>
>
Aah, it seems, the reason is wrong (my) definition of Mult: 2nd and 3rd
type family branches are not compatible: `Mult ('S 'Z) b` and `Mult ('S a1)
b` are not apart (hm.. probably; not sure what "arbitrary type-family
simplifications" means in [2], 6.2.1) and their RHS-es are not the same
"under the substitution induced by the unification" ([2], 6.2.1). And
because 2nd branch is not needed at all, all works fine with such Mult:

> type family Mult (a :: Nat) (b :: Nat) :: Nat where
>     Mult 'Z      b  = 'Z
>     Mult ('S a1) b  = Plus (Mult a1 b) b

[2]: https://wiki.haskell.org/GHC/Type_families#Closed_family_simplification
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20160316/b2494173/attachment.html>