I'm a newbie when it comes to the singleton
library, and may have bitten off more than I can chew here.
I've managed to use fromSing
successfully to convert a "singleton type" to a "value-level term" (is my terminology correct?) However, I'm unable to understand how to use toSing
and conceptually how it would convert a value at run-time to a type?
Here's what the docs for toSing
say, which I don't really understand...
-- Convert an unrefined type to an existentially-quantified singleton type.
toSing :: Demote k -> SomeSing k
Here's what SomeSing
says:
-- An existentially-quantified singleton. This type is useful
-- when you want a singleton type, but there is no way of knowing,
-- at compile-time, what the type index will be. To make use of this
-- type, you will generally have to use a pattern-match:
foo :: Bool -> ...
foo b = case toSing b of
SomeSing sb -> {- fancy dependently-typed code with sb -}
Does this mean that conceptually, fromSing
is basically doing the following:
data RuntimeValue = Value1 | Value2
someFunction :: RuntimeValue -> UnifiedType a
case runtimeValue of
Value1 -> someAction (Proxy :: Proxy 'Value1)
Value2 -> someAction (Proxy :: Proxy 'Value2)
And that is the best that one can expect from Haskell, as of today? i.e. we need to pattern-match on the runtime value, run functions that can be of different types, but ultimately they should unify to a single type?
If you compile the code:
{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
module SingletonExample where
import Data.Singletons.TH
singletons [d| data Value = Value1 | Value2 |]
with the flags -ddump-splices -dsuppress-uniques
, you can see the actual code the singletons
library is generating via Template Haskell. In particular, the generated SingKind
instance is:
instance SingKind Value where
type Demote Value = Value
fromSing SValue1 = Value1
fromSing SValue2 = Value2
toSing Value1 = SomeSing SValue1
toSing Value2 = SomeSing SValue2
So, fromSing
and toSing
are just boilerplate conversion functions from (runtime) values to (runtime) singletons and back.
That is, fromSing
and toSing
don't convert between values and types, they convert between values and singletons. You typically use toSing
when you have a function that's been written to require a singleton:
g :: SValue value -> String
g SValue1 = "one"
g SValue2 = "two"
but all you have is an associated value. In this case, you can use the somewhat awkward construct:
f :: Value -> String
f v = case toSing v of SomeSing sv -> g sv
to call g
with the requisite singleton.
It turns out that for the usual use cases for singletons, there are only a few situations where this works and/or is helpful. As a result, it's actually pretty rare to see toSing
used in singleton code. And, in particular, it's neither necessary nor very often particularly useful to use toSing
when working with types that are runtime-dependent.
Ultimately, if you want to learn/understand the singletons
library, you need to understand when and why singletons are useful (and the complex and subtle sense in which they are runtime representations of types), not how to convert back and forth between them and their associated values. To that end, I suggest reading the Hasochism paper, Dependently Typed Programming with Singletons, searching for "dependently typed programming in haskell" and or "haskell singletons" and reading every blog post you see. Weirich has some YouTube videos that would be worth checking out, too.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With