Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Is there a use case for `newtype T = MkT (T -> T)`?

Tags:

haskell

The paper "System F with Type Equality Coercions" by Sulzmann, Chakravarty, and Peyton Jones illustrates the translation of Haskell's newtype into System FC with the following example:

newtype T = MkT (T -> T)

As I understand it, barring unsafePerformIO, the only possible values of this type are MkT id and MkT undefined because of parametricity. I'm curious if there are some actual uses for this (or a similar) definition.

like image 398
Mikhail Glushenkov Avatar asked Dec 04 '12 03:12

Mikhail Glushenkov


People also ask

How long will the bear market last?

With this date as the start of the current official bear market, the average bear market of 289 days means that it would finish on 19th October 2022. So there you go, the bear market will end, based on the historical average, in the Fall and the good times will be back by Christmas.

Are strips a good investment?

STRIPS provides an alternative to traditional bonds for investors who need to rely on definite amounts of money coming due at a specific future date. Although they post negative cash flows until maturity, they may also provide superior yields to traditional bonds in some cases and will always mature at face value.

What is market share and why is it important?

Market Share is, very simply, the percentage of a certain sector that your product, service or software is responsible for, calculated by sales. Market share is used to give you an idea of how large, powerful or important your business is within its particular sector.

What are the 3 main parts of GTM?

The components of a go-to-market strategy are simple: market intelligence, market segmentation and product messaging.


1 Answers

Parametricity is about the values of types with variables. T has no variables, so parametricity does not apply. Infact, T has many inhabitants

ap :: T -> T -> T
ap (MkT f) t = f t

idT :: T
idT = MkT id

constT :: T
constT = MkT $ \t -> MkT $ \_ -> t

axiom_sT :: T
axiom_sT = MkT $ \f -> MkT $ \g -> MkT $ \a -> (g `ap` a) `ap` (f `ap` a)

The type T is an implementation of the Untyped Lambda Calculus, a universal formal system equivalent in power to a Turing machine. The three functions above (plus ap) form the SKI calculus, an equivalent formal system.

It is possible to encode any Haskell datatype into T. Consider the type for natural numbers

data Nat = Zero | Succ Nat

we can encode Nat into T

church :: Nat -> T
church Zero     = MkT $ \f -> MkT $ \x -> x
church (Succ n) = MkT $ \f -> MkT $ \x -> f `ap` (church n)

now, you are partially correct though. There is no way in Haskell to write the inverse function of this (so far as I know). Which is really a shame. Although you can write a sort of psuedo inverse with the type T -> IO Nat. Also, my understanding is the GHCs optimizer can die on recursive newtypes (someone please correct me if I am wrong about this, because I would like to go back to using them).

Instead, the type

data T = MkT (T -> T) | Failed String

with

ap (MkT f)    a = f a
ap (Failed s) _ = Failed s

which is the lambda calculus with exceptions, can be used in a fully invertable way.

In conclusion, in one sense T is not a useful type at all, but in another sense it is the most useful type of all.

like image 101
Philip JF Avatar answered Sep 19 '22 13:09

Philip JF