[Haskell-cafe] help with existential type signature?

[Jakob Brünker]

Hi Ken,

ideally, you'd want something like

f1 :: TypeLits.SomeNat -> exists n . Foo n

to indicate that this function will produce a Foo with some natural number,
but you don't know beforehand what that number is.
However, Haskell doesn't have built-in existential quantification (yet), so
you have to use some encoding that uses existing features instead.

There's at least two ways to do this. The first is to use an "existential
data type":

data SomeFoo = forall n . MkSomeFoo (Foo n)

You'll notice that it's named quite similarly to SomeNat - that's because
SomeNat is also an existential data type.
Then you could have a function like

showSomeFoo :: SomeFoo -> String
showSomeFoo (MkSomeFoo x) = show x

The other way is to pass in a function that tells f1 what to do with Foo it
produces:

  f1 :: TypeLits.SomeNat -> (forall fn . Foo fn -> a) -> a
  f1 mynat f = case mynat of {
    TypeLits.SomeNat (_ :: Proxy n) -> let {
      x :: Foo n;
      x = Mkfoo;
    } in f x
  };

In this case, you could call `f1 someNat show` to show a Foo made from
someNat.

These two encodings are equally powerful, but sometimes one is more
convenient than the other.

Cheers,

Jakob

On Sat, Feb 20, 2021 at 12:22 PM Ken T Takusagawa <kenta at mit.edu> wrote:

> {-
> I am experimenting with type-level naturals and with moving
> values known at runtime to type space.
>
> Is there a type signature that I can add to f1 below so that
> this will compile (maybe also requiring some additional
> LANGUAGE pragmas)?
>
> If I were to change the return value of f1 from "x" to "show
> x", then the program does compile, suggesting that there's
> nothing inherently wrong with "x".  But I'd prefer the
> option to compose the output of f1 with other computations
> separately, e.g., "show . f1" .
>
> Thanks,
> Ken
>
> -}
>
> {-# LANGUAGE KindSignatures, ScopedTypeVariables, DataKinds, Rank2Types #-}
> import qualified GHC.TypeLits as TypeLits;
> import Data.Proxy(Proxy);
> main = undefined;
>
> data Foo (fn :: TypeLits.Nat) = Mkfoo deriving (Show);
>
> --f1 :: TypeLits.SomeNat -> ? ;
> f1 mynat = case mynat of {
>   TypeLits.SomeNat (_ :: Proxy n) -> let {
>     x :: Foo n;
>     x = Mkfoo;
>   } in x
> };
>
> {-
> typelits.hs:27:8: error:
>     * Couldn't match expected type `p' with actual type `Foo n'
>         because type variable `n' would escape its scope
>       This (rigid, skolem) type variable is bound by
>         a pattern with constructor:
>           TypeLits.SomeNat :: forall (n :: TypeLits.Nat).
>                               TypeLits.KnownNat n =>
>                               Proxy n -> TypeLits.SomeNat,
>         in a case alternative
>         at smalltypelits2.hs:24:3-33
>     * In the expression: x
>       In the expression:
>         let
>           x :: Foo n
>           x = Mkfoo
>         in x
>       In a case alternative:
>           TypeLits.SomeNat (_ :: Proxy n)
>             -> let
>                  x :: Foo n
>                  x = Mkfoo
>                in x
>     * Relevant bindings include
>         x :: Foo n (bound at smalltypelits2.hs:26:5)
>         f1 :: TypeLits.SomeNat -> p (bound at smalltypelits2.hs:23:1)
>    |
> 27 |   } in x
>    |        ^
> -}
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210220/2adc543d/attachment.html>