On Mon, May 4, 2015 at 3:24 AM, Keean Schupke <[email protected]> wrote:
> On 4 May 2015 at 00:23, Matt Oliveri <[email protected]> wrote:
>> Since you said your existantials have a runtime witness, I can tell
>> you already that they are a dead wrong way of doing dependent types.
>> One of the major draws of dependent types is moving evidence and
>> checks to compile time. E.g. array bounds and bounds checking.
>
> You cannot move such things to compile time checking, because you don't know
> what they are until runtime.
>From your response below, it seems like you don't understand what
dependent typing is.
>> > types depending on values = existentials
>>
>> No. This is dependent types. This is exactly dependent types. We can
>> talk about what existential-like types various systems have later.
>> Dependent typing is conceptually prior to any specific type
>> constructor. But understanding abstract types is conceptually prior to
>> dependent typing.
>
> data Box = forall a . Show a => Box a
>
> Things we put in the box, once in the box, we cannot know the type of (at
> compile time) this is the meaning of not allowing the type variable to
> escape. However we do know the type at runtime, we can prove that:
>
> f (Box a) = show a
>
> Calling 'f' on a boxed value calls the correct version of show. So here we
> have a type depending on a value, whatever value is put in the box.
Now what on Earth makes you think this is a type depending on a value?
Because the Show instance is determined at runtime?
Let me be very explicit: dependent typing is when an expression
denoting a type can have a subexpression denoting an element of a
type.
The reasons this can be shortened to "types depending on values" is:
- Static types look at expressions, and don't technically know or care
about runtime.
- "depend on" is meant in the mathematical sense: The result of an
operation depends on the operands. In the syntax of a functional
language, this means an expression depends on its subexpressions.
- "values" means elements of types. They may or may not be known at
compile time. And again, we're talking about expressions, so
value-level variables count.
Of course dependent typing is not just meaningless syntax. But first,
you need to know the syntax.
> We can
> put a value in the box at runtime using polymorphic recursion:
>
> {-# LANGUAGE ExistentialQuantification #-}
>
> data Z = Z deriving Show
> data S x = S x deriving Show
>
> data Box = forall a . Show a => Box a
>
> reify' :: Show a => a -> Int -> Box
> reify' a 0 = Box a
> reify' a x | x > 0 = reify' (S a) (x - 1)
>
> reify x = reify' Z x
>
> main = do
> a <- (fmap read getLine) :: IO Int
> return $ let b = reify a in case b of
> Box c -> show c
No, none of that's dependent types. Note that Haskell doesn't have
dependent types. Some extensions to Haskell mimic them, but you're not
doing that either.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
