number-parameterized types and heterogeneous lists

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
9 messages Options
Reply | Threaded
Open this post in threaded view
|

number-parameterized types and heterogeneous lists

Harald ROTTER

Dear Haskellers,

after reading Oleg Kiselyov's paper on number-parameterized types I started
to play around with
the class Digits that encodes decimal numbers in types. The "typed number"
10 would e.g. be defined as

      D1 $ D0 $ Sz

I wondered if it would be possible replace the expression above by a
heterogeneous list like

      [D1,D0]

so I tried to define

      data Digit = forall a b.(Digits a, Digits (b a)) => Digit (a -> b a)

Loading this into ghci yields:

:t Digit D0

<interactive>:1:0:
    Ambiguous type variable `a' in the constraint:
      `Digits a' arising from a use of `Digit' at <interactive>:1:0-7
    Probable fix: add a type signature that fixes these type variable(s)

Removing the type constraints in the definition of "Digit":

      data Digit = forall a b.Digit (a -> b a)

makes it work like this:

      :t Digit D0
      Digit D0 :: Digit

      :t [Digit D0, Digit D1]
      [Digit D0, Digit D1] :: [Digit]

"Digit", however, is far too general (it also includes e.g. \x -> [x]), but
I would like it to be restricted to the Digit class.

Any help is appreciated.

Thanks

Harald.


CODE:

module Test where

data D0 a = D0 a
data D1 a = D1 a
data D2 a = D2 a
data D3 a = D3 a
data D4 a = D4 a
data D5 a = D5 a
data D6 a = D6 a
data D7 a = D7 a
data D8 a = D8 a
data D9 a = D9 a

class Digits ds where
    d2num :: Num a => ds -> a -> a

data Sz = Sz    -- zero size
instance Digits Sz where
    d2num _ acc = acc

instance Digits ds => Digits (D0 ds) where
    d2num dds acc = d2num (t22 dds) (10*acc)
instance Digits ds => Digits (D1 ds) where
    d2num dds acc = d2num (t22 dds) (10*acc+1)
instance Digits ds => Digits (D2 ds) where
    d2num dds acc = d2num (t22 dds) (10*acc+2)
instance Digits ds => Digits (D3 ds) where
    d2num dds acc = d2num (t22 dds) (10*acc+3)
instance Digits ds => Digits (D4 ds) where
    d2num dds acc = d2num (t22 dds) (10*acc+4)
instance Digits ds => Digits (D5 ds) where
    d2num dds acc = d2num (t22 dds) (10*acc+5)
instance Digits ds => Digits (D6 ds) where
    d2num dds acc = d2num (t22 dds) (10*acc+6)
instance Digits ds => Digits (D7 ds) where
    d2num dds acc = d2num (t22 dds) (10*acc+7)
instance Digits ds => Digits (D8 ds) where
    d2num dds acc = d2num (t22 dds) (10*acc+8)
instance Digits ds => Digits (D9 ds) where
    d2num dds acc = d2num (t22 dds) (10*acc+9)

t22 :: f x -> x
t22 = undefined

--data Digit = forall a b.(Digits a, Digits (b a)) => Digit (a -> b a)
data Digit = forall a b.Digit (a -> b a)

-------------------------------------------------------------------------------------------------



" Ce courriel et les documents qui y sont attaches peuvent contenir des informations confidentielles. Si vous n'etes  pas le destinataire escompte, merci d'en informer l'expediteur immediatement et de detruire ce courriel  ainsi que tous les documents attaches de votre systeme informatique. Toute divulgation, distribution ou copie du present courriel et des documents attaches sans autorisation prealable de son emetteur est interdite."

" This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, please advise the sender immediately and delete this e-mail and all attached documents from your computer system. Any unauthorised disclosure, distribution or copying hereof is prohibited."
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: number-parameterized types and heterogeneous lists

Anton Tayanovskyy
Hi Harald,

Can you give a link to the paper? Interesting stuff. Thanks.

This is stretching my abilities a bit, but is this what you are after?

data Digit = forall b.(Digits (b Sz)) => Digit (Sz -> b Sz)

instance Digits [Digit] where
    d2num []           acc = acc
    d2num (Digit x:xs) acc = d2num xs (10*acc + d2num (x Sz) 0)

I assumed you only want D0..D9 as digits, maybe this is too narrow.

I've put this up on hpaste:

http://hpaste.org/8437#a1



Bests,

Anton



On Fri, Jun 20, 2008 at 3:01 PM, Harald ROTTER <[hidden email]> wrote:

>
> Dear Haskellers,
>
> after reading Oleg Kiselyov's paper on number-parameterized types I started
> to play around with
> the class Digits that encodes decimal numbers in types. The "typed number"
> 10 would e.g. be defined as
>
>      D1 $ D0 $ Sz
>
> I wondered if it would be possible replace the expression above by a
> heterogeneous list like
>
>      [D1,D0]
>
> so I tried to define
>
>      data Digit = forall a b.(Digits a, Digits (b a)) => Digit (a -> b a)
>
> Loading this into ghci yields:
>
> :t Digit D0
>
> <interactive>:1:0:
>    Ambiguous type variable `a' in the constraint:
>      `Digits a' arising from a use of `Digit' at <interactive>:1:0-7
>    Probable fix: add a type signature that fixes these type variable(s)
>
> Removing the type constraints in the definition of "Digit":
>
>      data Digit = forall a b.Digit (a -> b a)
>
> makes it work like this:
>
>      :t Digit D0
>      Digit D0 :: Digit
>
>      :t [Digit D0, Digit D1]
>      [Digit D0, Digit D1] :: [Digit]
>
> "Digit", however, is far too general (it also includes e.g. \x -> [x]), but
> I would like it to be restricted to the Digit class.
>
> Any help is appreciated.
>
> Thanks
>
> Harald.
>
>
> CODE:
>
> module Test where
>
> data D0 a = D0 a
> data D1 a = D1 a
> data D2 a = D2 a
> data D3 a = D3 a
> data D4 a = D4 a
> data D5 a = D5 a
> data D6 a = D6 a
> data D7 a = D7 a
> data D8 a = D8 a
> data D9 a = D9 a
>
> class Digits ds where
>    d2num :: Num a => ds -> a -> a
>
> data Sz = Sz    -- zero size
> instance Digits Sz where
>    d2num _ acc = acc
>
> instance Digits ds => Digits (D0 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc)
> instance Digits ds => Digits (D1 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+1)
> instance Digits ds => Digits (D2 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+2)
> instance Digits ds => Digits (D3 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+3)
> instance Digits ds => Digits (D4 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+4)
> instance Digits ds => Digits (D5 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+5)
> instance Digits ds => Digits (D6 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+6)
> instance Digits ds => Digits (D7 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+7)
> instance Digits ds => Digits (D8 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+8)
> instance Digits ds => Digits (D9 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+9)
>
> t22 :: f x -> x
> t22 = undefined
>
> --data Digit = forall a b.(Digits a, Digits (b a)) => Digit (a -> b a)
> data Digit = forall a b.Digit (a -> b a)
>
> -------------------------------------------------------------------------------------------------
>
>
>
> " Ce courriel et les documents qui y sont attaches peuvent contenir des informations confidentielles. Si vous n'etes  pas le destinataire escompte, merci d'en informer l'expediteur immediatement et de detruire ce courriel  ainsi que tous les documents attaches de votre systeme informatique. Toute divulgation, distribution ou copie du present courriel et des documents attaches sans autorisation prealable de son emetteur est interdite."
>
> " This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, please advise the sender immediately and delete this e-mail and all attached documents from your computer system. Any unauthorised disclosure, distribution or copying hereof is prohibited."
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: number-parameterized types and heterogeneous lists

Harald ROTTER
In reply to this post by Harald ROTTER
Hello,

sorry for the late answer, I was off for the weekend :-)

The paper "Number-parameterized types" by Oleg Kielyov is located at

      http://okmij.org/ftp/papers/number-parameterized-types.pdf

It impressively shows what one can do with Haskell's type system.
What I am after is the replacement of a "chain" of digits, like e.g.
      D1 $ D0 $ D0 $ Sz
by a list
      [D1,D0,D0]
so I can effectively use list operations on those "typed numbers". I also
wonder if there is some kind of
"generalized" foldr such that, e.g.
      D1 $ D0 $ D0 $ Sz = specialFoldr ($) Sz [D1,D0,D0]
I think that this foldr must be some "special" foldr that augments the data
type of the result in each foldr step.
Would this be possible or am I just chasing phantoms ?

Thanks

Harald.



" Ce courriel et les documents qui y sont attaches peuvent contenir des informations confidentielles. Si vous n'etes  pas le destinataire escompte, merci d'en informer l'expediteur immediatement et de detruire ce courriel  ainsi que tous les documents attaches de votre systeme informatique. Toute divulgation, distribution ou copie du present courriel et des documents attaches sans autorisation prealable de son emetteur est interdite."

" This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, please advise the sender immediately and delete this e-mail and all attached documents from your computer system. Any unauthorised disclosure, distribution or copying hereof is prohibited."
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: number-parameterized types and heterogeneous lists

Luke Palmer-2
On Mon, Jun 23, 2008 at 6:50 AM, Harald ROTTER <[hidden email]> wrote:

> Hello,
>
> sorry for the late answer, I was off for the weekend :-)
>
> The paper "Number-parameterized types" by Oleg Kielyov is located at
>
>      http://okmij.org/ftp/papers/number-parameterized-types.pdf
>
> It impressively shows what one can do with Haskell's type system.
> What I am after is the replacement of a "chain" of digits, like e.g.
>      D1 $ D0 $ D0 $ Sz
> by a list
>      [D1,D0,D0]
> so I can effectively use list operations on those "typed numbers". I also
> wonder if there is some kind of
> "generalized" foldr such that, e.g.
>      D1 $ D0 $ D0 $ Sz = specialFoldr ($) Sz [D1,D0,D0]
> I think that this foldr must be some "special" foldr that augments the data
> type of the result in each foldr step.
> Would this be possible or am I just chasing phantoms ?

Mostly I believe you are.  What you are describing is firmly in the
realm of dependent types, far beyond Haskell's type system. See
Epigram or Agda for languages which have attempted to tackle this
problem.

Luke
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: number-parameterized types and heterogeneous lists

Bugzilla from alfonso.acosta@gmail.com
In reply to this post by Harald ROTTER
Inspired in Oleg's ideas, I implemented the packages type-level and
parameterized-data (which includes number-parameterized vectors).


To get an idea about how they work you might want to read their
haddock documentation in hackage:

http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-level
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/parameterized-data

You can get their darcs repositories (including some minor updates) from:

darcs get http://code.haskell.org/type-level
darcs get http://code.haskell.org/parameterized-data

On Fri, Jun 20, 2008 at 8:01 AM, Harald ROTTER <[hidden email]> wrote:

>
> Dear Haskellers,
>
> after reading Oleg Kiselyov's paper on number-parameterized types I started
> to play around with
> the class Digits that encodes decimal numbers in types. The "typed number"
> 10 would e.g. be defined as
>
>      D1 $ D0 $ Sz
>
> I wondered if it would be possible replace the expression above by a
> heterogeneous list like
>
>      [D1,D0]
>
> so I tried to define
>
>      data Digit = forall a b.(Digits a, Digits (b a)) => Digit (a -> b a)
>
> Loading this into ghci yields:
>
> :t Digit D0
>
> <interactive>:1:0:
>    Ambiguous type variable `a' in the constraint:
>      `Digits a' arising from a use of `Digit' at <interactive>:1:0-7
>    Probable fix: add a type signature that fixes these type variable(s)
>
> Removing the type constraints in the definition of "Digit":
>
>      data Digit = forall a b.Digit (a -> b a)
>
> makes it work like this:
>
>      :t Digit D0
>      Digit D0 :: Digit
>
>      :t [Digit D0, Digit D1]
>      [Digit D0, Digit D1] :: [Digit]
>
> "Digit", however, is far too general (it also includes e.g. \x -> [x]), but
> I would like it to be restricted to the Digit class.
>
> Any help is appreciated.
>
> Thanks
>
> Harald.
>
>
> CODE:
>
> module Test where
>
> data D0 a = D0 a
> data D1 a = D1 a
> data D2 a = D2 a
> data D3 a = D3 a
> data D4 a = D4 a
> data D5 a = D5 a
> data D6 a = D6 a
> data D7 a = D7 a
> data D8 a = D8 a
> data D9 a = D9 a
>
> class Digits ds where
>    d2num :: Num a => ds -> a -> a
>
> data Sz = Sz    -- zero size
> instance Digits Sz where
>    d2num _ acc = acc
>
> instance Digits ds => Digits (D0 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc)
> instance Digits ds => Digits (D1 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+1)
> instance Digits ds => Digits (D2 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+2)
> instance Digits ds => Digits (D3 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+3)
> instance Digits ds => Digits (D4 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+4)
> instance Digits ds => Digits (D5 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+5)
> instance Digits ds => Digits (D6 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+6)
> instance Digits ds => Digits (D7 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+7)
> instance Digits ds => Digits (D8 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+8)
> instance Digits ds => Digits (D9 ds) where
>    d2num dds acc = d2num (t22 dds) (10*acc+9)
>
> t22 :: f x -> x
> t22 = undefined
>
> --data Digit = forall a b.(Digits a, Digits (b a)) => Digit (a -> b a)
> data Digit = forall a b.Digit (a -> b a)
>
> -------------------------------------------------------------------------------------------------
>
>
>
> " Ce courriel et les documents qui y sont attaches peuvent contenir des informations confidentielles. Si vous n'etes  pas le destinataire escompte, merci d'en informer l'expediteur immediatement et de detruire ce courriel  ainsi que tous les documents attaches de votre systeme informatique. Toute divulgation, distribution ou copie du present courriel et des documents attaches sans autorisation prealable de son emetteur est interdite."
>
> " This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, please advise the sender immediately and delete this e-mail and all attached documents from your computer system. Any unauthorised disclosure, distribution or copying hereof is prohibited."
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: number-parameterized types and heterogeneous lists

Anton Tayanovskyy
Alfonso,

Thanks! For didactic purposes I will defer looking into your code. It
does not always help to know the correct solution :)


Bests,

--A

On Mon, Jun 23, 2008 at 11:26 AM, Alfonso Acosta
<[hidden email]> wrote:

> Inspired in Oleg's ideas, I implemented the packages type-level and
> parameterized-data (which includes number-parameterized vectors).
>
>
> To get an idea about how they work you might want to read their
> haddock documentation in hackage:
>
> http://hackage.haskell.org/cgi-bin/hackage-scripts/package/type-level
> http://hackage.haskell.org/cgi-bin/hackage-scripts/package/parameterized-data
>
> You can get their darcs repositories (including some minor updates) from:
>
> darcs get http://code.haskell.org/type-level
> darcs get http://code.haskell.org/parameterized-data
>
> On Fri, Jun 20, 2008 at 8:01 AM, Harald ROTTER <[hidden email]> wrote:
>>
>> Dear Haskellers,
>>
>> after reading Oleg Kiselyov's paper on number-parameterized types I started
>> to play around with
>> the class Digits that encodes decimal numbers in types. The "typed number"
>> 10 would e.g. be defined as
>>
>>      D1 $ D0 $ Sz
>>
>> I wondered if it would be possible replace the expression above by a
>> heterogeneous list like
>>
>>      [D1,D0]
>>
>> so I tried to define
>>
>>      data Digit = forall a b.(Digits a, Digits (b a)) => Digit (a -> b a)
>>
>> Loading this into ghci yields:
>>
>> :t Digit D0
>>
>> <interactive>:1:0:
>>    Ambiguous type variable `a' in the constraint:
>>      `Digits a' arising from a use of `Digit' at <interactive>:1:0-7
>>    Probable fix: add a type signature that fixes these type variable(s)
>>
>> Removing the type constraints in the definition of "Digit":
>>
>>      data Digit = forall a b.Digit (a -> b a)
>>
>> makes it work like this:
>>
>>      :t Digit D0
>>      Digit D0 :: Digit
>>
>>      :t [Digit D0, Digit D1]
>>      [Digit D0, Digit D1] :: [Digit]
>>
>> "Digit", however, is far too general (it also includes e.g. \x -> [x]), but
>> I would like it to be restricted to the Digit class.
>>
>> Any help is appreciated.
>>
>> Thanks
>>
>> Harald.
>>
>>
>> CODE:
>>
>> module Test where
>>
>> data D0 a = D0 a
>> data D1 a = D1 a
>> data D2 a = D2 a
>> data D3 a = D3 a
>> data D4 a = D4 a
>> data D5 a = D5 a
>> data D6 a = D6 a
>> data D7 a = D7 a
>> data D8 a = D8 a
>> data D9 a = D9 a
>>
>> class Digits ds where
>>    d2num :: Num a => ds -> a -> a
>>
>> data Sz = Sz    -- zero size
>> instance Digits Sz where
>>    d2num _ acc = acc
>>
>> instance Digits ds => Digits (D0 ds) where
>>    d2num dds acc = d2num (t22 dds) (10*acc)
>> instance Digits ds => Digits (D1 ds) where
>>    d2num dds acc = d2num (t22 dds) (10*acc+1)
>> instance Digits ds => Digits (D2 ds) where
>>    d2num dds acc = d2num (t22 dds) (10*acc+2)
>> instance Digits ds => Digits (D3 ds) where
>>    d2num dds acc = d2num (t22 dds) (10*acc+3)
>> instance Digits ds => Digits (D4 ds) where
>>    d2num dds acc = d2num (t22 dds) (10*acc+4)
>> instance Digits ds => Digits (D5 ds) where
>>    d2num dds acc = d2num (t22 dds) (10*acc+5)
>> instance Digits ds => Digits (D6 ds) where
>>    d2num dds acc = d2num (t22 dds) (10*acc+6)
>> instance Digits ds => Digits (D7 ds) where
>>    d2num dds acc = d2num (t22 dds) (10*acc+7)
>> instance Digits ds => Digits (D8 ds) where
>>    d2num dds acc = d2num (t22 dds) (10*acc+8)
>> instance Digits ds => Digits (D9 ds) where
>>    d2num dds acc = d2num (t22 dds) (10*acc+9)
>>
>> t22 :: f x -> x
>> t22 = undefined
>>
>> --data Digit = forall a b.(Digits a, Digits (b a)) => Digit (a -> b a)
>> data Digit = forall a b.Digit (a -> b a)
>>
>> -------------------------------------------------------------------------------------------------
>>
>>
>>
>> " Ce courriel et les documents qui y sont attaches peuvent contenir des informations confidentielles. Si vous n'etes  pas le destinataire escompte, merci d'en informer l'expediteur immediatement et de detruire ce courriel  ainsi que tous les documents attaches de votre systeme informatique. Toute divulgation, distribution ou copie du present courriel et des documents attaches sans autorisation prealable de son emetteur est interdite."
>>
>> " This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, please advise the sender immediately and delete this e-mail and all attached documents from your computer system. Any unauthorised disclosure, distribution or copying hereof is prohibited."
>> _______________________________________________
>> Haskell-Cafe mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: number-parameterized types and heterogeneous lists

Ryan Ingram
In reply to this post by Luke Palmer-2
Literate haskell response:
> {-# LANGUAGE GADTs, RankNTypes #-}
> module Digits where
> {-

On 6/23/08, Luke Palmer <[hidden email]> wrote:

> > I also wonder if there is some kind of "generalized" foldr such that, e.g.
> >      D1 $ D0 $ D0 $ Sz = specialFoldr ($) Sz [D1,D0,D0]
> > I think that this foldr must be some "special" foldr that augments the data
> > type of the result in each foldr step.
> > Would this be possible or am I just chasing phantoms ?

> Mostly I believe you are.  What you are describing is firmly in the
> realm of dependent types, far beyond Haskell's type system. See
> Epigram or Agda for languages which have attempted to tackle this
> problem.

> -}

I'm not so sure, as long as you are willing to live with the result
being existentially quantified.  Here's an example:
ghci> mkNat [x1, x0, x3, x2]
(reifyInt 1032)
ghci> :t mkNat [x1, x0, x3, x2]
mkNat [x1, x0, x3, x2] :: AnyNat

I slightly specialize the constructors to wrap them in existential types:
d0 = AnyNat . D0  -- and so on for d1..d9
x0 = NatFn d0 -- and so on for x1..x9


Full code:

> data Sz = Sz
> data D0 a = D0 a
> data D1 a = D1 a
> data D2 a = D2 a
> data D3 a = D3 a
> data D4 a = D4 a
> data D5 a = D5 a
> data D6 a = D6 a
> data D7 a = D7 a
> data D8 a = D8 a
> data D9 a = D9 a

> class Nat n where
>    toIntAccum :: n -> Integer -> Integer

> toInt :: Nat n => n -> Integer
> toInt n = toIntAccum n 0

> instance Nat Sz where toIntAccum _ acc = acc

> instance Nat a => Nat (D0 a) where
>     toIntAccum (D0 n) acc = toIntAccum n (10 * acc + 0)
> instance Nat a => Nat (D1 a) where
>     toIntAccum (D1 n) acc = toIntAccum n (10 * acc + 1)
> instance Nat a => Nat (D2 a) where
>     toIntAccum (D2 n) acc = toIntAccum n (10 * acc + 2)
> instance Nat a => Nat (D3 a) where
>     toIntAccum (D3 n) acc = toIntAccum n (10 * acc + 3)
> instance Nat a => Nat (D4 a) where
>     toIntAccum (D4 n) acc = toIntAccum n (10 * acc + 4)
> instance Nat a => Nat (D5 a) where
>     toIntAccum (D5 n) acc = toIntAccum n (10 * acc + 5)
> instance Nat a => Nat (D6 a) where
>     toIntAccum (D6 n) acc = toIntAccum n (10 * acc + 6)
> instance Nat a => Nat (D7 a) where
>     toIntAccum (D7 n) acc = toIntAccum n (10 * acc + 7)
> instance Nat a => Nat (D8 a) where
>     toIntAccum (D8 n) acc = toIntAccum n (10 * acc + 8)
> instance Nat a => Nat (D9 a) where
>     toIntAccum (D9 n) acc = toIntAccum n (10 * acc + 9)

> data AnyNat where AnyNat :: Nat n => n -> AnyNat

> d0, d1, d2, d3, d4, d5, d6, d7, d8, d9 :: Nat n => n -> AnyNat
> d0 = AnyNat . D0
> d1 = AnyNat . D1
> d2 = AnyNat . D2
> d3 = AnyNat . D3
> d4 = AnyNat . D4
> d5 = AnyNat . D5
> d6 = AnyNat . D6
> d7 = AnyNat . D7
> d8 = AnyNat . D8
> d9 = AnyNat . D9

> reifyDigit :: Integer -> (forall n. Nat n => n -> AnyNat)
> reifyDigit 0 = d0
> reifyDigit 1 = d1
> reifyDigit 2 = d2
> reifyDigit 3 = d3
> reifyDigit 4 = d4
> reifyDigit 5 = d5
> reifyDigit 6 = d6
> reifyDigit 7 = d7
> reifyDigit 8 = d8
> reifyDigit 9 = d9
> reifyDigit _ = error "not a digit"

> reifyIntAccum :: Integer -> AnyNat -> AnyNat
> reifyIntAccum 0 acc          = acc
> reifyIntAccum n (AnyNat rhs) = let (l, r) = divMod n 10 in
>                                reifyIntAccum l (reifyDigit r rhs)

> reifyInt :: Integer -> AnyNat
> reifyInt n | n < 0  = error "negative"
> reifyInt n          = reifyIntAccum n (AnyNat Sz)

> instance Show AnyNat where
>     show (AnyNat n) = "(reifyInt " ++ show (toInt n) ++ ")"

> data NatFn where NatFn :: (forall n. Nat n => n -> AnyNat) -> NatFn

> x0, x1, x2, x3, x4, x5, x6, x7, x8, x9 :: NatFn
> x0 = NatFn d0
> x1 = NatFn d1
> x2 = NatFn d2
> x3 = NatFn d3
> x4 = NatFn d4
> x5 = NatFn d5
> x6 = NatFn d6
> x7 = NatFn d7
> x8 = NatFn d8
> x9 = NatFn d9

> foldNat :: [NatFn] -> AnyNat -> AnyNat
> foldNat []           z = z
> foldNat (NatFn f:xs) z = case foldNat xs z of AnyNat n -> f n

> mkNat :: [NatFn] -> AnyNat
> mkNat xs = foldNat xs (AnyNat Sz)

  -- ryan
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: number-parameterized types and heterogeneous lists

oleg-30
In reply to this post by Harald ROTTER

Luke Palmer wrote in response to Harald ROTTER
> > I also wonder if there is some kind of "generalized" foldr such that, e.g.
> >      D1 $ D0 $ D0 $ Sz = specialFoldr ($) Sz [D1,D0,D0]
> > I think that this foldr must be some "special" foldr that augments the data
> > type of the result in each foldr step.
> > Would this be possible or am I just chasing phantoms ?

> Mostly I believe you are.  What you are describing is firmly in the
> realm of dependent types, far beyond Haskell's type system. See
> Epigram or Agda for languages which have attempted to tackle this
> problem.

First of all, Haskell (as implemented by released versions of GHC for
at least two years) already permits dependent types, in the
strict sense of a type of an expression being determined by the value
of one argument of that expression:

        http://okmij.org/ftp/Computation/tagless-typed.html#tc-GADT-tc

Second, (values of) types like D0 and D1 can be collected in a
heterogenous list (HList), which does have the corresponding fold
operator, called HFoldr in

        http://darcs.haskell.org/HList/Data/HList/HListPrelude.hs

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: number-parameterized types and heterogeneous lists

Harald ROTTER
In reply to this post by Harald ROTTER

Hello Anton,

thanks for your enlightening piece of code. "foldD" does exactly what I was
hoping for.
Now it becomes very obvious to me that the positions of the forall's in the
Digit definition are crucial.

Thanks a lot to Alfonso, Luke and Ryan as well. Haskell Cafe is a really
good place to learn new things :-)

Harald.



" Ce courriel et les documents qui y sont attaches peuvent contenir des informations confidentielles. Si vous n'etes  pas le destinataire escompte, merci d'en informer l'expediteur immediatement et de detruire ce courriel  ainsi que tous les documents attaches de votre systeme informatique. Toute divulgation, distribution ou copie du present courriel et des documents attaches sans autorisation prealable de son emetteur est interdite."

" This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, please advise the sender immediately and delete this e-mail and all attached documents from your computer system. Any unauthorised disclosure, distribution or copying hereof is prohibited."
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe