従属型のインスタンスを表示する

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をユーザー提供の文字列から作成します。まず、シングルトンからアドレスを取得します。ちょうど今のところ1本の弦を取る

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 ""はaの場合はKnownSymbol aとなりますが、GHCはSymbol -sを含むすべての種類のプログラムを消去するため、このようなことは起こりません。 aに対応するランタイムStringを呼び出すことはできません。これが最初にシングルトンを使用する必要がある理由です。

別の観点から、String -> EmailAddress a aの問題は、我々は、特定のaためKnownSymbol a出力を必要とするので、入力Stringは、いかなる意味のある方法で使用することができないということです。

シングルトンでないランタイムデータがある場合は、それをtoSingという実在シングルトンに変換することができます。次に、結果のシングルトンのプロパティについて学習するためにランタイムチェックを実行することができます。