显示依赖类型的实例

Question

我在 ghc 8 中使用依赖类型，但在为我的类型创建 Show 实例时遇到了问题。

#!/usr/bin/env stack
-- stack exec --resolver=lts-7.14 --package singletons -- ghci
{-# LANGUAGE GADTs, ScopedTypeVariables, TypeInType, TemplateHaskell, LambdaCase, TypeApplications #-}

import Data.Kind
import Data.Singletons.Prelude
import Data.Singletons.TypeLits

 data EmailAddress :: Symbol -> Symbol -> * where
  EmailAddress :: (KnownSymbol a, KnownSymbol b) => EmailAddress a b 

-- works
testEmail :: EmailAddress "blah" "blah.com"
testEmail = EmailAddress

我希望能够显示我的地址。

instance Show (EmailAddress a b)
  where show = showEmailAddress

showEmailAddress :: forall a b. EmailAddress a b -> String
showEmailAddress = \case
  EmailAddress -> symbolVal (Proxy :: Proxy a) ++ "@" ++ symbolVal (Proxy :: Proxy b)

test1 = show testEmail -- works

现在我想从用户提供的字符串创建一个运行时EmailAddress。首先，我将从单身人士那里得到一个地址。暂时只取一根绳子。

fromString' :: Sing i -> EmailAddress i i
fromString' = \case
  SSym -> EmailAddress

test2 = fromString' @"asdf" sing -- works

难题的最后一块是我觉得我应该能够执行以下操作。

fromString :: String -> EmailAddress a a
fromString str = case toSing str of
   SomeSing s -> fromString' s

但它不起作用。无论我对函数的各个部分应用什么类型签名，我都无法对其进行类型检查，我总是在以下代码中收到以下错误Couldn't match type ‘a’ with ‘a1’ 错误。

fromString1 :: String -> EmailAddress a a
fromString1 str = case toSing str of
   SomeSing s -> fromString' s

fromString2 :: forall a. String -> EmailAddress a a
fromString2 str = case toSing str of
   SomeSing (s :: Sing a) -> fromString' s

fromString3 :: forall a. String -> EmailAddress a a
fromString3 str = case toSing str of
   (SomeSing s :: Sing (a :: Symbol)) -> fromString' s

这是完整的错误。我不明白a1 是从哪里来的。

Existentials5.hs:45:20: error:
• Couldn't match type ‘a’ with ‘a1’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      fromString3 :: forall (a :: Symbol). String -> EmailAddress a a
    at Existentials5.hs:43:16
  ‘a1’ is a rigid type variable bound by
    a pattern with constructor:
      SomeSing :: forall k k1 (k2 :: k1) (a :: k). Sing a -> SomeSing k,
    in a case alternative
    at Existentials5.hs:45:5
  Expected type: EmailAddress a a
    Actual type: EmailAddress a1 a1
• In the expression: fromString' s
  In a case alternative: (SomeSing s) -> fromString' s
  In the expression:
    case toSing str of { (SomeSing s) -> fromString' s }
• Relevant bindings include
    s :: Sing a1 (bound at Existentials5.hs:45:14)
    fromString3 :: String -> EmailAddress a a
      (bound at Existentials5.hs:44:1)

Answer 1

fromString :: String -> EmailAddress a a 是不可能的。 fromString @a "" 会给我们KnownSymbol a 任何a，这是不可能的，因为GHC 会从程序中删除所有类型，包括Symbol-s。我们不能只是想出一个对应于a 的运行时String。这就是我们必须首先使用单例的原因。

从另一个角度来看，String -> EmailAddress a a 的问题在于输入 String 不能以任何有意义的方式使用，因为我们需要一个特定 a 的 KnownSymbol a 输出。

如果我们有非单例运行时数据，我们可以使用toSing 将其转换为存在单例。然后我们可以进行运行时检查以了解生成的单例的属性。