On Tue, Mar 15, 2016 at 1:23 PM, Dmitriy Matrosov
{-# 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-safet...
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