Hi John Meacham wrote:
On Mon, Oct 23, 2006 at 03:26:33PM +0100, Conor McBride wrote:
This seems like the ideal time to make a wannabe library proposal which is pointless, but pointless by design. The code's quite short:
so, just to clarify, is what you are proposing is a type whose only inhabitant is _|_, and since _|_ inhabits all types, we should be able to freely cast this bottom-only-containing type to any other?
Exactly, although I prefer to avoid talking about _|_ unless I absolutely have to. The fact that there are no values worth speaking of in |Zero| is a good way of pinning down the /absence/ of things, hence the use of |Tm Zero| to represent terms with no free variables. Moreover, general tree-like structures given by fixpoints of functors
data Fix f = In (f (Fix f))
have a general notion of |leaf|
leaf :: Functor f => f Zero -> Fix f leaf = In . fMagic
If you're interested in calculating types of one-hole contexts, then |Zero| is very handy
class (Functor f, Functor g) => Diff f g | f -> g where ...
instance Diff (Const c) (Const Zero) where ... instance Diff Id (Const ()) where ... instance (Diff f f', Diff g g') => Diff (Sum f g) (Sum f' g') where ... instance (Diff f f', Diff g g') => Diff (Prod f g) (Sum (Prod f' g) (Prod f g')) where ...
where Sum and Prod are Either and (,) lifted pointwise to kind * -> *
Sounds good to me. I can't think of a use off the top of my head, but I ended up using Identity all over the place... and this sounds like just the random sort of thing I will find odd uses for. :)
so plenty of odd uses!
but since 'Zero' is often used in type arithmetic implementations (even though those uses arn't entirely incompatable) I think we should name it something else.
I think the two go very well together. If you define
data Suc n = New | Old n
then the type-level unary numbers double as types with that many values worth speaking of. I'm rather fond of the idea that |Tm (Suc (Suc Zero))| is the type of terms in two free variables, and so on. You also get that addition, multiplication, etc, for type-level numbers correspond to, er, sum, product, etc for the types. I know this kind of breaks the singleton hack to give run-time proxies for static types, but there are other ways to make proxies.
I think
data Bottom
is waht I would like.
This is one thing we've got that we shouldn't flaunt. If I can't have Zero, please may I have
data Naught
naughty :: Naught -> y
innocent :: Functor f => f Naught -> f x
or some such? Cheers Conor This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.