Home » forums » LtU Forum

What is this type of type called?

Often restricted data types are used as jails. For example, the IO monad in Haskell can't let any impure value escape. Sometimes however, even though it is not safe to release any value from the jail in general it is possible for some specific values.

As an example, for some type T one might want to allow a function of the type "(T a -> T b) -> (a -> b)", but not a function of the type "T a -> a".

Another example, which is trivial, is that one might allow data of the type,(using Coq's notation for types where the values are constrained by propositions), "{ x : IO a | forsome y, x = pure y }" to escape where pure is the function of the type "a -> IO a".

What is it called when a data type can't be extracted from but a more complex data type built up from it can?

By Steven StewartGallus at 2011-12-15 18:54 | LtU Forum | previous forum topic | next forum topic | other blogs | 7959 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Intuition deficit

I'm not sure I understand the intuition behind the first example:

Observe that if

(1) (T a -> T b) -> (a -> b)

and we have the monadic theorem

(2) TT a -> T a

together with modus ponens (type application), then

(3) T a -> a

is a theorem, by instantiating (1) to get

(4) (TT a -> T a) -> (T a-> a)

and applying to (2).

You seem to be after a property of type systems, rather than a kind of type.

By Charles Stewart at Fri, 2011-12-16 09:37 | login or register to post comments

Not sure your proof works

He did not say that T is a monad, so it's not clear why you assume (2).

In general, it seems to me that he's just describing a very general notion of "type constructor with some operations" which could be satisfied by lots of common type classes in Haskell. Take an opaque type constructor and expose a few functions operating on it, maybe provide instances for some named classes (e.g., Monoid, Applicative, Traversable...) and isn't this just what he's describing?

So I'm not sure if "abstract data type" or "functor with some laws" is a good name, but I'm not sure there's a better one.

By Matt Hellige at Fri, 2011-12-16 14:53 | login or register to post comments

And incidentally...

I'm not sure that first example was intended to be "real" or was just off the cuff. It seems a bit fishy to me as well...

By Matt Hellige at Fri, 2011-12-16 14:54 | login or register to post comments

Assumption discharged

Well, I discharged my assumption of (2) —although I admittedly did not discharge my assumption of type variable instantiation, which I guess some contrived type system might not satisfy— I just said that if the T and -> satisfied certain properties, the distinction wouldn't hold.

If you want to look at it like a puzzle, then find a type system that has an instance of (1) without satisfying (3). I'm more interested in the intuition that led Steven to ask the question.

By Charles Stewart at Fri, 2011-12-16 21:01 | login or register to post comments

Hmm...

I guess I think he intended something like the following in Haskell:

class Foo t where
  unwrap :: (t a -> t b) -> (a -> b)

data Bar a = Close { open :: a }

instance Foo Bar where
  unwrap bf = open . bf . Close

I don't see how to write a function with a type like: Foo f => f a -> a. Obviously unwrap has an instance at (f f a -> f a) -> f a -> a, but you can't produce the argument, so what difference does it make?

Of course, there's nothing else that can be done with Foo, either, but that doesn't make it inherently unreasonable.

By Matt Hellige at Fri, 2011-12-16 21:51 | login or register to post comments

crack :: Foo t => t a -> a


crack ta = unwrap (const ta) ()

By Matt M at Fri, 2011-12-16 22:36 | login or register to post comments

That example was a simplification

I know that if one actually to do that one would need a different function. I've come up with several variations on the idea of how to prevent one extracting from the type T in that case but there all more complex, and I'm not sure if they work either so I just went with the simple example.

One idea I had was having an extra variable r, so the function would be this "(forall r. T r a -> T r b) -> a -> b". I have no clue if that works either, and I wouldn't know how to prove it did even if it did. See my post asking how to prove a type systems safety.

By Steven StewartGallus at Sat, 2011-12-17 01:22 | login or register to post comments

Needs more info

It's not clear to me what it would even mean for that type to work. Can you elaborate on your motivations like Charles and Matt suggested?

By Matt M at Sat, 2011-12-17 02:48 | login or register to post comments

Oh yeah...

Funny, I had a sinking feeling as I typed the words "I don't see how to..."

I guess that's what I get for disregarding one of my mottos: "Never argue with logicians on a Friday."

By Matt Hellige at Sat, 2011-12-17 03:35 | login or register to post comments