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. Re: Programming with Singletons (mukesh tiwari)
2. argument counts... (Gregory Guthrie)
----------------------------------------------------------------------
Message: 1
Date: Fri, 17 Nov 2017 19:06:36 +1100
From: mukesh tiwari <[email protected]>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <[email protected]>
Subject: Re: [Haskell-beginners] Programming with Singletons
Message-ID:
<cafhzve8ud7skdi71+dk+4nnermnpfhdez+8v4qu_suwp+qq...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
Disregard my previous mail, because I realized that your Sub is correct
except (Succ a). Sorry for the confusion. New definition below
type family (Sub (a :: Nat) (b :: Nat)) :: Nat
type instance Sub a Zero = a
type instance Sub Zero b = Zero
type instance Sub (Succ a) (Succ b) = Sub a b
On Fri, Nov 17, 2017 at 1:08 PM, mukesh tiwari <[email protected]
> wrote:
> Changed your Sub code to this and drop works now. You drop function
> drop SZero vcons = vcons so you are returning the second
> vector if first one is empty (length Zero).
>
>
> type family (Sub (a :: Nat) (b :: Nat)) :: Nat
> type instance Sub a Zero = a
> type instance Sub Zero b = b
> type instance Sub (Succ a) (Succ b) = Sub a b
>
> No use of Min in your code, but I changed it anyway.
>
> type family (Min (a :: Nat) (b :: Nat)) :: Nat
> type instance Min Zero b = Zero
> type instance Min a Zero = Zero
> type instance Min (Succ a) (Succ b) = Succ (Min a b)
>
> I am not able to compile your tail code, so could you please paste your
> whole code github, or any preferred link which you like.
> I am getting
>
> *Not in scope: type constructor or class ‘:<’*
>
> On Fri, Nov 17, 2017 at 12:01 PM, Quentin Liu <[email protected]>
> wrote:
>
>> Thank you so much! Indeed changing the definition of `Add` helps solve
>> the problem.
>>
>> Following this idea, I changed the definition of `Minus` and `Min` also.
>> Now they are defined as
>>
>> type family (Sub (a :: Nat) (b :: Nat)) :: Nat
>> type instance Sub (Succ a) Zero = Succ a
>> type instance Sub Zero b = Zero
>> type instance Sub (Succ a) (Succ b) = Sub a b
>>
>> type family (Min (a :: Nat) (b :: Nat)) :: Nat
>> type instance Min Zero Zero = Zero
>> type instance Min Zero (Succ b) = Zero
>> type instance Min (Succ a) Zero = Zero
>> type instance Min (Succ a) (Succ b) = Succ (Min a b)
>>
>>
>> The change, however, breaks the `tail` and `drop` function.
>>
>> drop :: SNat a -> Vec s b -> Vec s (Sub b a)
>> drop SZero vcons = vcons
>> drop (SSucc a) (VCons x xs) = drop a xs
>>
>> tail :: ((Zero :< a) ~ True) => Vec s a -> Vec s (Sub a (Succ Zero))
>> tail (VCons x xs) = xs
>>
>>
>> So why does the code break and what would be the solution? The error
>> message seems to confirm that even right now GHD still does not support
>> type expansion.
>>
>> Regards,
>> Qingbo Liu
>>
>> On Nov 15, 2017, 19:51 -0500, mukesh tiwari <[email protected]
>> >, wrote:
>>
>> Hi Quentin,
>> I changed your pattern little bit in Add function and it is working
>> fine. I think the problem was that type of (VCons x xs) ++++ b is Vec
>> v (Add (Succ m1) + n) which was not present in your
>> Add function pattern.
>>
>>
>>
>> {-# LANGUAGE TypeFamilies #-}
>> {-# LANGUAGE DataKinds #-}
>> {-# LANGUAGE KindSignatures #-}
>> {-# LANGUAGE GADTs #-}
>> {-# LANGUAGE InstanceSigs #-}
>> module Tmp where
>>
>> data Nat = Zero | Succ Nat
>>
>> data SNat a where
>> SZero :: SNat Zero
>> SSucc :: SNat a -> SNat (Succ a)
>>
>> data Vec a n where
>> VNil :: Vec a Zero
>> VCons :: a -> Vec a n -> Vec a (Succ n)
>>
>> type family (Add (a :: Nat) (b :: Nat)) :: Nat
>> type instance Add Zero b = b
>> type instance Add (Succ a) b = Succ (Add a b)
>>
>> (++++) :: Vec v m -> Vec v n -> Vec v (Add m n)
>> VNil ++++ b = b
>> (VCons x xs) ++++ b = VCons x $ xs ++++ b
>>
>> On Thu, Nov 16, 2017 at 11:21 AM, Quentin Liu
>> <[email protected]> wrote:
>>
>> Hi all,
>>
>> I was doing the “Singletons” problem at codewars[1]. The basic idea is to
>> use dependent types to encode the length of the vector in types.
>>
>> It uses
>> data Nat = Zero | Succ Nat
>>
>> data SNat a where
>> SZero :: SNat Zero
>> SSucc :: SNat a -> SNat (Succ a)
>> to do the encoding.
>>
>> The vector is defined based on the natural number encoding:
>> data Vec a n where
>> VNil :: Vec a Zero
>> VCons :: a -> Vec a n -> Vec a (Succ n)
>>
>>
>> There are some type families declared for manipulating the natural
>> numbers,
>> and one of them that is relevant to the question is
>> type family (Add (a :: Nat) (b :: Nat)) :: Nat
>> type instance Add Zero b = b
>> type instance Add a Zero = a
>> type instance Add (Succ a) (Succ b) = Succ (Succ (Add a b))
>> where the `Add` function adds natural numbers.
>>
>> The problem I am stuck with is the concatenation of two vectors:
>> (++) :: Vec v m -> Vec v n -> Vec v (Add m n)
>> VNil ++ b = b
>> (VCons x xs) ++ b = VCons x $ xs ++ b
>>
>> The program would not compile because the compiler found that `VCons x $
>> xs
>> ++ b`gives type `Vec v (Succ (Add n1 n))`, which does not follow the
>> declared type `Vec v (Add m n)`. Is it because ghc does not expand `Add m
>> n’
>> that the type does not match? I read Brent Yorgey’s blog on type-level
>> programming[2] and he mentioned that would not automatically expand types.
>> But the posted time of the blog is 2010 and I am wondering if there is any
>> improvement to the situation since then? Besides, what would be the
>> solution
>> to this problem
>>
>>
>> Warm Regards,
>> Qingbo Liu
>>
>> [1] https://www.codewars.com/kata/singletons/train/haskell
>> [2]
>> https://byorgey.wordpress.com/2010/07/06/typed-type-level-pr
>> ogramming-in-haskell-part-ii-type-families/
>>
>>
>> _______________________________________________
>> Beginners mailing list
>> [email protected]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>>
>> _______________________________________________
>> Beginners mailing list
>> [email protected]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>>
>>
>> _______________________________________________
>> Beginners mailing list
>> [email protected]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20171117/bbf6f91c/attachment-0001.html>
------------------------------
Message: 2
Date: Fri, 17 Nov 2017 02:35:00 -0600
From: Gregory Guthrie <[email protected]>
To: "[email protected]" <[email protected]>
Subject: [Haskell-beginners] argument counts...
Message-ID:
<[email protected]>
Content-Type: text/plain; charset="utf-8"
I have a simple function:
revFn (x:xs) = (revFn xs) . (x:)
Of course GHCi correctly infers the type as: revFn :: [a] -> [a] -> c
Adding the base case:
revFn [] xs = xs
Now gives an error;
"Equations for 'revF' have different numbers of arguments"
Of course this can be "fixed" by either adding the cancelled argument to the
first clause, or converting the base case to only have one explicit argument,
and a RHS of a lambda or identity function.
But since the interpreter already correctly inferred that the first clause has
two arguments (with only one explicit), why does it then ignore this and give
an error when the second clause shows two explicit arguments? The types are all
correct in either case - why require explicit arguments?
Or, perhaps I am missing something simple?
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20171117/4da43592/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 113, Issue 15
******************************************
