Send Beginners mailing list submissions to
[email protected]
To subscribe or unsubscribe via the World Wide Web, visit
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
[email protected]
You can reach the person managing the list at
[email protected]
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Multiplicaton of singletons (Dmitriy Matrosov)
----------------------------------------------------------------------
Message: 1
Date: Tue, 15 Mar 2016 13:23:00 +0300
From: Dmitriy Matrosov <[email protected]>
To: [email protected]
Subject: [Haskell-beginners] Multiplicaton of singletons
Message-ID:
<CAFdVUF=d3wttgxqcdo+3up6vah1mcfmss7x6bh0bqy86h+z...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
> {-# 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20160315/8695d8a9/attachment-0001.html>
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 93, Issue 10
*****************************************
