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

[Andras Slemmer]

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150515/aa4ee11e/attachment-0001.html>