[Haskell-cafe] Data constructor ‘Minus’ comes from an un-promotable type ‘Ints’

Tue May 19 05:50:13 UTC 2015

Wow, that's exciting news!
18 трав. 2015 16:05 "Richard Eisenberg" <eir at cis.upenn.edu> пише:

>
> On May 18, 2015, at 5:02 AM, "Nicholls, Mark" <nicholls.mark at vimn.com>
> wrote:
>
>
> The problem being the any definition containing promoted types, cannot be
> promoted.
>
> Is that a fair summary?
>
>
> Yes. Only "simple" types can be promoted.
>
> But this will all change in 7.12, where just about anything will promote.
> For now, you may want to switch to Agda, but come back in a year's time. :)
>
> Richard
>
>
>
> *From:* Haskell-Cafe [mailto:haskell-cafe-bounces at haskell.org] *On Behalf
> Of *Nicholls, Mark
> *Sent:* 15 May 2015 1:35 PM
> *To:* Andras Slemmer
> *Cc:* haskell-cafe at haskell.org
> *Subject:* Re: [Haskell-cafe] Data constructor ‘Minus’ comes from an
> un-promotable type ‘Ints’
>
> Its inhabited, and I can potentials readon about positive and negative and
> zero…because these are mapped to type constructors….but they are not
> isomorphic to the integers…they are just 3 sub classes of the class of
> integers…
>
> That aint much good.
>
> I assume its because the even the type of my data constructor Zero is…
>
> Ints 'Z 'Z
>
> If I wanted an isomorphic type constructor…it would need to be?
>
> 'Ints ''Z ''Z
>
> (I know haskell doesn’t promote the type Ints to a kind ‘Ints, it
> irritatingly promotes it to Ints….)
>
> ‘’Z doesn’t exist…?
>
> hmmm
>
>
> *From:* Nicholls, Mark
> *Sent:* 15 May 2015 1:03 PM
> *To:* 'Andras Slemmer'
> *Cc:* 'haskell-cafe at haskell.org'
> *Subject:* RE: [Haskell-cafe] Data constructor ‘Minus’ comes from an
> un-promotable type ‘Ints’
>
> Ignore me…of course it’s inhabited…..
>
> *From:* Nicholls, Mark
> *Sent:* 15 May 2015 12:58 PM
> *To:* 'Andras Slemmer'
> *Cc:* haskell-cafe at haskell.org
> *Subject:* RE: [Haskell-cafe] Data constructor ‘Minus’ comes from an
> un-promotable type ‘Ints’
>
> Ah, ok that’s a vote for agda.
>
> Your ints definition isn’t directly inhabited…..but maybe that doesn’t
> matter….thanks I’ll struggle on a bit.
>
> (yes my definition is mildly problematic mathematically, I have 3
> (coincident) zeros).
>
> *From:* Andras Slemmer [mailto:0slemi0 at gmail.com <0slemi0 at gmail.com>]
> *Sent:* 15 May 2015 10:50 AM
> *To:* Nicholls, Mark
> *Cc:* haskell-cafe at haskell.org
> *Subject:* Re: [Haskell-cafe] Data constructor ‘Minus’ comes from an
> un-promotable type ‘Ints’
>
>
> If you want to stick to your Ints datastructure then you need a stronger
> dependent type theory that allows you to reason about "double-promoted"
> types.
>
> However in this case you don't really need that complexity:
>
> data Ints
>   = Zero
>   | Minus Nat
>   | Plus Nat
> is sufficient enough. Although this definition is probably not the one you
> want to use... take a look at
> http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Integer.agda for hints
>
> On 14 May 2015 at 18:36, Nicholls, Mark <nicholls.mark at vimn.com> wrote:
> Hello,
>
> I clearly don’t really know what I’m doing…but at least I know it….
>
> Here we defined the Naturals…and then attempt to construct the Integers….
>
> > {-# LANGUAGE DataKinds #-}
> > {-# LANGUAGE ExplicitForAll #-}
> > {-# LANGUAGE FlexibleContexts #-}
> > {-# LANGUAGE FlexibleInstances #-}
> > {-# LANGUAGE GADTs #-}
> > {-# LANGUAGE MultiParamTypeClasses #-}
> > {-# LANGUAGE PolyKinds #-}
> > {-# LANGUAGE StandaloneDeriving #-}
> > {-# LANGUAGE TypeFamilies #-}
> > {-# LANGUAGE TypeOperators #-}
> > {-# LANGUAGE UndecidableInstances #-}
> > {-# LANGUAGE ScopedTypeVariables #-}
>
> > import Prelude hiding (head, tail, (++), (+), replicate)
> > import qualified Prelude as P
>
> naturals
>
> > data Nat where
> >   Z :: Nat
> >   S :: Nat -> Nat
>
> I can now define + and * and prove things about them…1 * x == x
> etc….nice..but lets put that on one side.
>
> Borrow bits and bobs from singletons
>
> > data family Sing (a :: k)
>
> Borrow bits and bobs from singletons..i.e. the isomorphic values…my proofs
> in nat now map to SNat…double nice.
>
> > type SNat = (Sing :: Nat -> *)
>
> Create the integers by following my nose……(the integers are the
> equivalence class of pairs of naturals….)
>
> i.e. we have “positive” or “negative” or “zero”…
>
> > data Ints (a :: Nat) (b :: Nat) where
> >   Minus :: SNat a -> Ints 'Z a
> >   Zero :: Ints 'Z 'Z
> >   Plus :: SNat a -> Ints a 'Z
> >
>
> Ok….this works as a set of values….but….
>
> I can’t prove anything about these because the data constructors for my
> integers aren’t “promotable”…..so I cant do the same trick I did with Nat.
>
> “:k Zero” …..
>     Data constructor ‘Zero’ comes from an un-promotable type ‘Ints’
>     In a type in a GHCi command: Zero
>
> I’ve tried rejigging this in various futile and ignorant manners….but the
> bottom line is its…”un-promotable”…..look at the docs, and it says
> something vague about GADT’s…but that isnt the problem directly.
>
> Is there a nifty way around this log jam?
> (I can start proving things about ‘(Nat,Nat)….but this will soon become a
> bit clumsy….)
>
> Or do I just stop here and wrestle with getting agda installed and lose
> another few months in the agda-café (which appears to be a very nice place
> somewhere in finland….hmmmm…I think that’s something different).
>
> (I’ve already allegedly descended into cabal hell following my nose with
> an agda install…
> setup.exe: The program cpphs version >=1.18.6 && <1.19 is required but the
> version found at C:\Users\nichom\AppData\Roaming\cabal\bin\cpphs.exe is
> version 1.19).
>
> computer science would be good, if it wasn’t for the computers.
>
>
>
>
>
>
> CONFIDENTIALITY NOTICE
>
> This e-mail (and any attached files) is confidential and protected by
> copyright (and other intellectual property rights). If you are not the
> intended recipient please e-mail the sender and then delete the email and
> any attached files immediately. Any further use or dissemination is
> prohibited.
>
> While MTV Networks Europe has taken steps to ensure that this email and
> any attachments are virus free, it is your responsibility to ensure that
> this message and any attachments are virus free and do not affect your
> systems / data.
>
> Communicating by email is not 100% secure and carries risks such as delay,
> data corruption, non-delivery, wrongful interception and unauthorised
> amendment. If you communicate with us by e-mail, you acknowledge and assume
> these risks, and you agree to take appropriate measures to minimise these
> risks when e-mailing us.
>
> MTV Networks International, MTV Networks UK & Ireland, Greenhouse,
> Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions
> International, Be Viacom, Viacom International Media Networks and VIMN and
> Comedy Central are all trading names of MTV Networks Europe.  MTV Networks
> Europe is a partnership between MTV Networks Europe Inc. and Viacom
> Networks Europe Inc.  Address for service in Great Britain is 17-29 Hawley
> Crescent, London, NW1 8TT.
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>
>
>
> CONFIDENTIALITY NOTICE
>
> This e-mail (and any attached files) is confidential and protected by
> copyright (and other intellectual property rights). If you are not the
> intended recipient please e-mail the sender and then delete the email and
> any attached files immediately. Any further use or dissemination is
> prohibited.
>
> While MTV Networks Europe has taken steps to ensure that this email and
> any attachments are virus free, it is your responsibility to ensure that
> this message and any attachments are virus free and do not affect your
> systems / data.
>
> Communicating by email is not 100% secure and carries risks such as delay,
> data corruption, non-delivery, wrongful interception and unauthorised
> amendment. If you communicate with us by e-mail, you acknowledge and assume
> these risks, and you agree to take appropriate measures to minimise these
> risks when e-mailing us.
>
> MTV Networks International, MTV Networks UK & Ireland, Greenhouse,
> Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions
> International, Be Viacom, Viacom International Media Networks and VIMN and
> Comedy Central are all trading names of MTV Networks Europe.  MTV Networks
> Europe is a partnership between MTV Networks Europe Inc. and Viacom
> Networks Europe Inc.  Address for service in Great Britain is 17-29 Hawley
> Crescent, London, NW1 8TT.
>
>
>
> CONFIDENTIALITY NOTICE
>
> This e-mail (and any attached files) is confidential and protected by
> copyright (and other intellectual property rights). If you are not the
> intended recipient please e-mail the sender and then delete the email and
> any attached files immediately. Any further use or dissemination is
> prohibited.
>
> While MTV Networks Europe has taken steps to ensure that this email and
> any attachments are virus free, it is your responsibility to ensure that
> this message and any attachments are virus free and do not affect your
> systems / data.
>
> Communicating by email is not 100% secure and carries risks such as delay,
> data corruption, non-delivery, wrongful interception and unauthorised
> amendment. If you communicate with us by e-mail, you acknowledge and assume
> these risks, and you agree to take appropriate measures to minimise these
> risks when e-mailing us.
>
> MTV Networks International, MTV Networks UK & Ireland, Greenhouse,
> Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions
> International, Be Viacom, Viacom International Media Networks and VIMN and
> Comedy Central are all trading names of MTV Networks Europe.  MTV Networks
> Europe is a partnership between MTV Networks Europe Inc. and Viacom
> Networks Europe Inc.  Address for service in Great Britain is 17-29 Hawley
> Crescent, London, NW1 8TT.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150519/532c776e/attachment-0001.html>